From Stateflow Simulation to Verified Implementation: A Verification Approach and A Real-Time Train Controller Design

Yu Jiang, Yixiao Yang, Han Liu, Hui Kong, Ming Gu, Jiaguang Sun, Lui Sha

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

Abstract

Simulink is widely used for model driven development (MDD) of industrial software systems. Typically, the Simulink based development is initiated from Stateflow modeling, followed by simulation, validation and code generation mapped to physical execution platforms. However, recent industrial trends have raised the demands of rigorous verification on safety-critical applications, which is unfortunately challenging for Simulink. In this paper, we present an approach to bridge the Stateflow based model driven development and a well- defined rigorous verification. First, we develop a self- contained toolkit to translate Stateflow model into timed automata, where major advanced modeling features in Stateflow are supported. Taking advantage of the strong verification capability of Uppaal, we can not only find bugs in Stateflow models which are missed by Simulink Design Verifier, but also check more important temporal properties. Next, we customize a runtime verifier for the generated nonintrusive VHDL and C code of Stateflow model for monitoring. The major strength of the customization is the flexibility to collect and analyze runtime properties with a pure software monitor, which opens more opportunities for engineers to achieve high reliability of the target system compared with the traditional act that only relies on Simulink Polyspace. We incorporate these two parts into original Stateflow based MDD seamlessly. In this way, safety-critical properties are both verified at the model level, and at the consistent system implementation level with physical execution environment in consideration. We apply our approach on a train controller design, and the verified implementation is tested and deployed on a real hardware platform.

Original languageEnglish (US)
Title of host publication2016 IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2016 - Proceedings
PublisherInstitute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)9781467386395
DOIs
StatePublished - Apr 27 2016
EventIEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2016 - Vienna, Austria
Duration: Apr 11 2016Apr 14 2016

Publication series

Name2016 IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2016 - Proceedings

Other

OtherIEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2016
Country/TerritoryAustria
CityVienna
Period4/11/164/14/16

Keywords

  • Formal Verification
  • Model Driven Development
  • Runtime Verification
  • Simulink Stateflow
  • Timed Automaton

ASJC Scopus subject areas

  • Hardware and Architecture

Fingerprint

Dive into the research topics of 'From Stateflow Simulation to Verified Implementation: A Verification Approach and A Real-Time Train Controller Design'. Together they form a unique fingerprint.

Cite this