CoCoSim: Contract based Compositional verification of Simulink models

CoCoSim (Contract based Compositional verification of Simulink models) is used to verify user-supplied requirements. The main objective of CoCoSim is to provide the followings:

• A formal semantic for a well defined subset of Simulink/Stateflow blocks. This formal representation allows the use of formal verification methods and code generation. It also can be used as a semantic of reference for other tools. Find more about the formal semantics of Simulink/Stateflow used in the CoCoSim manual.
• A highly automated toolchain: all the steps of verification or code generation are automated, check CoCoSim manual.
• A Customizable and configurable architecture: Currently CoCosim supports most frequently used Simulink blocks libraries (> 100 blocks) either by transforming them to simpler blocks or by direct translation to a formal language. The translation is customizable and extensible; new blocks can be easily supported.
• Full traceability throughout the analysis process. This traceability is crucial in reporting analysis results expressed in the formal model back to the user in the context of the Simulink model. For instance, the Counter-examples generated by model checkers is reported back to the Simulink level using a Signal Builder block to help the user debug the internal Signals values.
• Scalability to large models: abtained through the use of various verification techniques and compositional reasoning.

Cocosim has an open architecture allowing for the integration of different analyses. The motivation is to support different verification techniques to scale to large models. CoCoSim can generate C and/or Rust code. CoCoSim uses multiple model checkers for verification including Zustre, Kind2, and JKind. CoCoSim is currently under development. We welcome any feedback, contributions and bug reports.

License

CoCoSim has been released under the NASA Open Source Agreement.

Contact

Please contact [email protected] or [email protected] for further information on CoCoSim. Detailed information can be found at the CoCoSim manual

Installation

Platforms

CoCoSim currently supports Mac OS and Linux. Future support is planned for Windows.

Dependencies and Installation instructions can be found here

Quick Start

Explanation of each CoCoSim feature can be found here

Release notes and work in progress

For release notes and what actually we are working on see here

Troubleshooting

Solution of some common issues with CoCoSim are here

Developers

• Project leader: Guillaume Brat (NASA Ames - USA), Pierre-Loic Garoche (ENAC - France)

• Lead Developer: Andreas Katis (KBR Inc at NASA Ames - USA)

• Past Contributors:
  Hamza Bourbouh, Khanh Trinh, Temesghen Kahsai, Maxime Arthaud, Francois Conzelmann

Publications

• Automated analysis of Stateflow models
  H Bourbouh, PL Garoche, C Garion, A Gurfinkel, T Kahsai, X Thirioux
  EasyChair 46, 144-161

• CoCoSim, a code generation framework for control/command applications. An overview of CoCoSim for multi-periodic discrete Simulink models
  H Bourbouh, PL Garoche, T Loquen, É Noulard, C Pagetti
  10th European Congress on Embedded Real Time Software and Systems (ERTS 2020)

• Evaluation of the FRET and CoCoSim tools on the Ten Lockheed Martin Cyber-Physical Challenge Problems
  A Mavridou, H Bourbouh, PL Garoche, M Hejase
  NASA Technial Report: NASA/TM-2019-220374

• Bridging the Gap Between Requirements and Simulink Model Analysis
  A Mavridou, H Bourbouh, PL Garoche, D Giannakopoulou, T Pressburger, J Schumann
  REFSQ2020