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

    Abstract

    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)
    PublisherIEEE
    ISBN (Electronic)9781479914432
    DOIs
    Publication statusPublished - 2013
    EventInternational Conference on Embedded Software 2013 - Montreal, Canada
    Duration: 29 Sep 20134 Oct 2013

    Conference

    ConferenceInternational Conference on Embedded Software 2013
    Abbreviated titleEMSOFT
    CountryCanada
    CityMontreal
    Period29/09/134/10/13

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

  • Cite this

    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