In Action


CoCoSim is a toolbox that can be called directly from the Matlab Simulink environment (similar to Simulink Design Verifier). CoCoSim can be used either for code generation (e.g. C/Rust and/or Lustre) or for property verification. The front-end performs a bunch of pre-processing (i.e. lowering of different Simulink blocks into basic blocks) and optimizations.
The compiler, translate modularly the pre-processed Simulink model and generates Lustre code. Moreover, it performs book-keeping of the different Simulink/Stateflow constructs (e.g. signal name, block type etc ..). This allows to trace Simulink/Stateflow constructs in the Lustre programs.
Takes the Lustre code and it performs either (i) compilation into imperative code (C or Rust) or (ii) it performs sfatey analysis of the provided property. For compilation it uses LustreC, while for safety verification it uses one of: Zustre, Kind2 or JKind. The result of the safety analysis is reported back to the Matlab environment. In case the property supplied is falsified, CoCoSim provides means to simulate the counterexample trace in the Matlab environment.