Simulink is an industrial de-facto standard for building executable models of embedded systems and their environments, 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 system dynamics by means of an extension of CSP. The translation from Simulink to HCSP is fully automatic. We furthermore discuss how to utilize a Hybrid Hoare Logic Prover to verify the translated HCSP models. We demonstrate our approach on a combined scenario originating from the Chinese High-speed Train Control System at Level 3 (CTCS-3).
|Title of host publication||2013 Proceedings of the International Conference on Embedded Software (EMSOFT)|
|Publication status||Published - 2013|
|Event||International Conference on Embedded Software 2013 - Montreal, Canada|
Duration: 29 Sep 2013 → 4 Oct 2013
|Conference||International Conference on Embedded Software 2013|
|Period||29/09/13 → 4/10/13|
Zou, L., Zhany, N., Wang, S., Fränzle, M., & Qin, S. (2013). Verifying Simulink diagrams via a Hybrid Hoare Logic Prover. In 2013 Proceedings of the International Conference on Embedded Software (EMSOFT) IEEE. https://doi.org/10.1109/EMSOFT.2013.6658587