Formal Semantic Specification of CPS modeling languages

Cyber-Physical Systems (CPS) are integration of computational and physical systems. CPS-s have many safety-critical applications, such as traffic control, aviation, power and chemical plants, or medical devices. In order to support the development of safe CPS-s, we need to unambiguously define the semantics of the modeling languages used for designing them.

The idea is summarized in the following picture. Modelica, Hybrid bond graphs, CyPhyML and ESMoL are modeling languages used for the design of CPS-s. Instead of developing our own tools for these languages, it is a better choice to reuse the existing state of the art solutions by mapping the modeling languages to the languages of the corresponding tools. Unless we have an unambiguous specification for the semantics of the modeling language, these mappings are ad hoc. Different developers may interpret the language in different ways, and the input model for the verification tool may differ from the generated implementation. We can tackle this problem by supplementing the modeling language with formal semantic specifications.

For more information about the problem and its background, please see this presentation.