A Generic Event-B Theory for the Formalisation of the International System of Units
摘要
Formal verification of cyber-physical systems (CPS) requires a model that accurately represents physical measurements from the real world. Incorporating explicit units into these measurements enhances rigour by enabling the verification of unit compatibility and correction in computations. While formal methods such as Event-B support static type checking, they lack the capability to annotate variables with physical measurement units. This paper proposes extending the Event-B type-checking system by defining a generic theory that offers the possibility to annotate Event-B variables with measurement units. This approach allows the specification of physical quantities, units, and measurements using the Theory plug-in.