Verifying Simulink diagrams via a Hybrid Hoare Logic Prover

Liang Zou, Naijun Zhany, Shuling Wang, Martin Fränzle, Shengchao Qin

    Research output: Chapter in Book/Report/Conference proceedingConference contribution


    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).
    Original languageEnglish
    Title of host publication 2013 Proceedings of the International Conference on Embedded Software (EMSOFT)
    ISBN (Electronic)9781479914432
    Publication statusPublished - 2013
    EventInternational Conference on Embedded Software 2013 - Montreal, Canada
    Duration: 29 Sept 20134 Oct 2013


    ConferenceInternational Conference on Embedded Software 2013
    Abbreviated titleEMSOFT


    Dive into the research topics of 'Verifying Simulink diagrams via a Hybrid Hoare Logic Prover'. Together they form a unique fingerprint.

    Cite this