NASA Logo, National Aeronautics and Space Administration

CoCoSim verification of TCM Simulink model

CoCoSim: Contract-based Compositional verification of Simulink models

CoCoSim is an automated analysis tool for verifying and validating Simulink and Stateflow models. CoCoSim can be used to automatically perform test case generation and to evaluate the validity of user-supplied safety requirements. CoCoSim can also be used to generate C and/or Rust code from Simulink or Stateflow models.

CoCoSim logo The main use of CoCoSim is to provide verification and validation of user-supplied Simulink or Stateflow programs. CoCoSim is structured to operate much like a compiler, sequencing a series of translation steps leading, eventually to either the production of source code, or to the call of a verification tool.

CoCoSim allows users to express safety properties as synchronous observers within the Simulink model or StateFlow Diagram. Synchronous observers are code segments that implement assume-guarantee reasoning by taking state variables as input and then producing one or more Boolean outputs. Synchronous observers are simply masked subsystems that compare inputs and outputs of a model to generate a logic True or False answer.

CoCoSim Benefits

  • Open-source, free software (that is customizable by the user) and offers almost the same features as SLDV
  • Supports most of discrete blocks and pre-processes some of continuous blocks..
  • Sacalability - whereas SLDV is limited to smaller code segments, CoCoSim can handle really big programs.
  • Customizable - CoCoSim supports Zustre, Kind2, and JKind bounded model checkers and the documentation on how to use them. It can be extended by customizing the existing libraries (such as pre-processing functions) or add more libraries and features
  • Compositionality - In one study, compositional verification using Kind2 was able to prove that more than 90% of the code was correct.
  • Test generation - CoCoSim also offers test-case generation to support evidence for MC/DC coverage and proof that requirements are correct.


CoCoSim has been used in the analysis of a commercial aircraft control system implemented as a large, high-fidelity, Simulink model that included avionics, (with transport delay), actuators, engines, landing gear, nonlinear aerodynamics, sensors (including noise), aircraft parameters, equations of motion, and gravity. The model consists of approximately 5700 Simulink blocks. CoCoSim was used to study the guidance and controls models and their properties. CoCoSim was used to verify 10 high-level safety requirements of the model. Five requirements were proved to be safe, while the other 5 were proved to be unsafe and counterexamples producing the unsafe states were provided).

Updated December 2017

Active Members

Hamza Bourbouh
Guillaume Brat
Pierre-Loic Garoche

Past Members

Temesghen Kahsai
Jorge Navas

Collaboration with ONERA

First Gov logo
NASA Logo -