oldenburg.de

Simulink is an industrial de-facto standard for building ex-ecutable models of embedded systems and their environ-ments, facilitating validation by simulation. Due to the inherent incompleteness of this form of system validation, complementing simulation by formal verification would be desirable. A prerequisite for such an approach is a formal semantics of Simulink’s graphical models. In this paper, we show how to encode Simulink diagrams into Hybrid CSP (HCSP), a formal modelling language encoding hybrid sys-tem dynamics by means of an extension of CSP. The transla-tion from Simulink to HCSP is fully automatic. We further-more discuss how to utilize a Hybrid Hoare Logic Prover to verify the translated HCSP models. We demonstrate our ap-proach on a combined scenario originating from the Chines