CoCoSim: Simulink Verification Framework(ARC-18277-1)

CoCoSim is a framework that integrates analysis technologies 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. The main use of CoCoSim is to provide verification and validation of 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 inputs and then producing one or more Boolean outputs indicating if the observer agrees with the behavior of the model.