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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

A Generic Event-B Theory for the Formalisation of the International System of Units

  • Idir Ait-Sadoune

摘要

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.