CPS: Breakthrough: Compositional System Modeling with Interfaces (COSMOI)

Design of cyber-physical systems today relies on executable models. Designers develop models, simulate them, find defects, and improve their designs before the system is built, thus greatly reducing the design costs. However, current model-based design methods lack support for model libraries (creating and exchanging models as "black boxes"), tool interoperability (allowing models to be co-simulated by multiple tools), and multi-view modeling (allowing to combine models that "live in different worlds", for instance, a control-logic model with an energy-consumption model). This project seeks to remedy this by developing a compositional modeling framework based on interfaces. Interfaces allow submodels to be treated as black boxes, exposing relevant information while hiding internal details. The project develops: (1) A formal and executable interface framework supporting major CPS modeling paradigms (discrete, continuous, dataflow, dynamic, acausal), as well as views. (2) Techniques for automatic interface checking and synthesis. Interface checking allows to check errors similarly to type-checking in programs, but it is more powerful as interfaces are dynamic, behavioral types. Interface synthesis allows to automatically generate the interface of a model from the interfaces of its submodels. (3) A formal framework for view composition. Views in this project are models, and particularly abstractions of other models.

Recent results of the project include:

• The Refinement Calculus of Reactive Systems (RCRS), a compositional framework for modeling and reasoning about CPS, including a fully formalized implementation on top of the Isabelle theorem prover that can handle real-world Simulink benchmarks.
• A rigorous co-simulation framework based on the FMI (Functional Mockup Interface) stan- dard and a prototype implementation in Ptolemy.
• A formal framework for multi-view modeling which allows to formulate problems such as view consistency, and algorithms to solve such problems.