*banner
 
 

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. 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,4,13,15,16,20,21].

  • Interfaces for co-simulation. References: [1,9,10,11,12,14,17,18,22,23].
  • Multi-view modeling. References: [1,5,6,19].

Intellectual merit and broader impacts

legos 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.

Funding source: COSMOI is a 4-year project (3 years + 1 year no-cost extension) funded by the NSF within the Cyber-Physical Systems (CPS) program. Award code CNS-1329759.

Duration: Oct. 1, 2013 -- Sep. 30, 2017.

People

Software

Publications

  1. Iulia Dragomir, Viorel Preoteasa, Stavros Tripakis. The Refinement Calculus of Reactive Systems Toolset. Oct 2017. Arxiv tech report.
  2. Viorel Preoteasa, Iulia Dragomir, Stavros Tripakis. The Refinement Calculus of Reactive Systems. Oct 2017. Arxiv tech report.
  3. Viorel Preoteasa, Iulia Dragomir, Stavros Tripakis. Type Inference of Simulink Hierarchical Block Diagrams in Isabelle. In FORTE 2017. Earlier/revised/extended version available as Arxiv tech report.
  4. Viorel Preoteasa, Iulia Dragomir, Stavros Tripakis. A Nondeterministic and Abstract Algorithm for Translating Hierarchical Block Diagrams. Nov 2016. Arxiv tech report.
  5. Stavros Tripakis. Compositionality in the Science of System Design. Proceedings of the IEEE. Special Issue on Industrial Cyber-Physical Systems. May 2016. Preprint.
  6. Viorel Preoteasa and Stavros Tripakis. Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems. Thirty-First Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). July 5-8, 2016, New York City, USA. Preprint.
  7. Georgios Giantamidis, Stavros Tripakis. Learning Moore Machines from Input-Output Traces. 21st International Symposium on Formal Methods (FM 2016). arxiv.org version.
  8. Iulia Dragomir, Viorel Preoteasa, Stavros Tripakis. Compositional Semantics and Analysis of Hierarchical Block Diagrams. 23rd International SPIN symposium on Model Checking of Software (SPIN 2016).
  9. Maria Pittou, Stavros Tripakis. Checking Multi-View Consistency of Discrete Systems with respect to Periodic Sampling Abstractions. Formal Aspects of Component Software - The 13th International Conference (FACS 2016).
  10. Maria Pittou, Stavros Tripakis. Multi-View Consistency for Infinitary Regular Languages. 2016 International Conference on Embedded Computer Systems: Architectures, Modeling and Simulation - SAMOS XVI.
  11. Srinivas Pinisetty, Stavros Tripakis. Compositional Runtime Enforcement. 8th NASA Formal Methods Symposium (NFM 2016). Preprint.
  12. Srinivas Pinisetty, Viorel Preoteasa, Stavros Tripakis, Thierry Jeron, Ylies Falcone, Herve Marchand. Predictive Runtime Enforcement. 31st ACM/SIGAPP Symposium on Applied Computing, Software Verification and Testing Track (SAC-SVT 2016).
  13. Fabio Cremona, Marten Lohstroh, David Broman, Marco Di Natale, Edward Lee, Stavros Tripakis. Step Revision in Hybrid Co-simulation with FMI. 14th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2016).
  14. Fabio Cremona, Marten Lohstroh, Stavros Tripakis, Christopher Brooks, Edward Lee. FIDE: an FMI integrated development environment. 31st ACM/SIGAPP Symposium on Applied Computing (SAC 2016).
  15. Sergiy Bogomolov, Marius Greitschus, Peter G. Jensen, Kim G. Larsen, Marius Mikucionis, Thomas Strump, and Stavros Tripakis. Co-Simulation of Hybrid Systems with SpaceEx and Uppaal. 11th International Modelica Conference, 2015.
  16. Stavros Tripakis. Bridging the Semantic Gap Between Heterogeneous Modeling Formalisms and FMI. Embedded Computer Systems: Architectures, Modeling and Simulation - SAMOS XV, 2015.
  17. Antti Siirtola, Stavros Tripakis, and Keijo Heljanko. When Do We (Not) Need Complex Assume-Guarantee Rules? 15th International Conference on Application of Concurrency to System Design (ACSD), 2015.
  18. David Broman, Lev Greenberg, Edward A. Lee, Michael Masin, Stavros Tripakis, and Michael Wetter. Requirements for Hybrid Cosimulation Standards. In Hybrid Systems: Computation and Control (HSCC), 2015.
  19. 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.
  20. 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.
  21. David Broman, Lev Greenberg, Edward A. Lee, Michael Masin, Stavros Tripakis and Michael Wetter. Requirements for Hybrid Cosimulation. EECS technical report, Aug 2014.
  22. Stavros Tripakis and David Broman. Bridging the Semantic Gap Between Heterogeneous Modeling Formalisms and FMI. EECS technical report, Apr 2014.
  23. 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.
  24. 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.
  25. 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).
  26. 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.
  27. 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.

Admins: To modify this page, use Subversion.

You are not logged in 
©2002-2017 Chess