Compositional System Modeling with Interfaces (COSMOI)

Stavros Tripakis and Edward A. Lee

National Science Foundation 1329759

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. This methodology is called Model Based Design (MBD). We may view the vision of MBD as being the development of a system compiler. 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), component-based reasoning (e.g., proving global correctness of a system by combining local properties of its components), and multi-view modeling (allowing to combine models that "live in different worlds", for instance, a control-logic model with an energy-consumption model). NSF project CPS: Breakthrough: Compositional System Modeling with Interfaces (COSMOI) 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 currently focuses on the following activities:

  • Interface theories and compositional verification. References: [1,2,6].
  • Interfaces for modeling and co-simulation. References: [3,4,8,9].
  • Multi-view modeling. References: [5].
Intellectual merit and broader impacts This project addresses the key problem of how to model cyber-physical systems in a scalable and modular manner. Success of the project will provide a solid theoretical foundation for CPS model composition. It will also enable the design of CPS model libraries, model exchange and tool interoperability. Finally, it will have a direct influence on the design of FMI, an emerging international standard with a high potential impact on CPS. Besides the considerable economic and societal impact of cyber-physical systems in general, the proposed project will have considerable impact on engineering and computer science education. Its focus on a rigorous and unified modeling theory will erode the boundaries between the currently separated cyber-physical system sub-disciplines that hamper competitiveness of our students. Finally, the project is strategically important for the competitiveness of the United States as it strengthens its presence in international standardization efforts for model exchange and co-simulation.

[1]
Pierluigi Nuzzo, Antonio Iannopollo, Stavros Tripakis, and Alberto L. Sangiovanni-Vincentelli. Are Interface Theories Equivalent to Contract Theories? In 12th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE), 2014. See also EECS technical report.
[2]
Viorel Preoteasa and Stavros Tripakis. Refinement Calculus of Reactive Systems. In 14th ACM and IEEE International Conference on Embedded Software (EMSOFT 2014). See also pre-print available as arxiv.org report.
[3]
Stavros Tripakis and David Broman. Bridging the Semantic Gap Between Heterogeneous Modeling Formalisms and FMI. EECS technical report, Apr 2014.
[4]
Jan Reineke and Stavros Tripakis. Basic Problems in Multi-View Modeling. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014). See also EECS technical report.
[5]
Stavros Tripakis and Chris Shaver. Feedback in Synchronous Relational Interfaces. In volume 8415 of Lecture Notes in Computer Science, From Programs to Systems, pages 249–266. Springer, 2014.
[6]
Antonio Iannopollo, Pierluigi Nuzzo, Stavros Tripakis, and Alberto Sangiovanni-Vincentelli. Library-Based Scalable Refinement Checking for Contract-Based Design. In Design and Test Europe (DATE 2014).
[7]
David Broman, Christopher Brooks, Lev Greenberg, Edward A. Lee, Stavros Tripakis, Michael Wetter, and Michael Masin. Determinate Composition of FMUs for Co-Simulation. In 13th ACM and IEEE International Conference on Embedded Software (EMSOFT 2013). See also EECS technical report.
[8]
Stavros Tripakis, Christos Stergiou, Chris Shaver, and Edward A. Lee. A Modular Formal Semantics for Ptolemy. In journal Mathematical Structures in Computer Science, Aug 2013.

More information: http://chess.eecs.berkeley.edu/cosmoi/