CoCoSim is an automated analysis and code generation framework for Simulink and Stateflow models. Specifically, CoCoSim can be used to verify automatically user-supplied safety requirements. Moreover, CoCoSim can be used to generate C and/or Rust code. CoCoSim uses Lustre as its intermediate language. CoCoSim is currently under development. We welcome any feedback and bug report.
Installation instructions can be found here.
- CoCoSim Specification Library
- CoCoSim Menu
- Supported Simulink Blocks
- Visualization of Verification Results
- Compositional Analysis
- Launch cocosim
start_cocosim - Open one of the examples
open('contract/DoorLockCompositional.slx') - To verify the model, go to Tools menu and select
Tools/CoCoSim/Verify
The first video below explains the concept of contract specification using a simple Lustre model that simulates the evolution of a bacteria population. The second video shows how CoCoSim can be used to specify a contract for a CoCoSim version of the bacteria population model. Finally, the third video explains the concept of compositional analysis using a semi-realistic model of a door lock.
-
Project leaders: Temesghen Kahsai, Cesare Tinelli, and Corina Pasareanu
-
Developers/Contributors: Hamza Bourbouh (SGT - USA), Pierre-Loic Garoche (Onera - France), Mudathir Mohamed (The University of Iowa - USA), Baoluo Meng (The University of Iowa - USA), Daniel Larraz (The University of Iowa - USA), Christelle Dambreville (ENSEEIHTENSEEIHT - France), Claire Pagetti (Onera - France), Eric Noulard (Onera - France), Thomas Loquen (Onera - France), Xavier Thirioux (ENSEEIHT - France), and Arnaud Dieumegard (IRIT - France)
CoCoSim was partially funded by:
- NASA NRA NNX14AI09G
- NSF award 1136008
Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) do not necessarily reflect the views of NASA and NSF.