TY - GEN
T1 - From Stateflow Simulation to Verified Implementation
T2 - IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2016
AU - Jiang, Yu
AU - Yang, Yixiao
AU - Liu, Han
AU - Kong, Hui
AU - Gu, Ming
AU - Sun, Jiaguang
AU - Sha, Lui
N1 - Publisher Copyright:
© 2016 IEEE.
PY - 2016/4/27
Y1 - 2016/4/27
N2 - 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.
AB - 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.
KW - Formal Verification
KW - Model Driven Development
KW - Runtime Verification
KW - Simulink Stateflow
KW - Timed Automaton
UR - http://www.scopus.com/inward/record.url?scp=84971320746&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84971320746&partnerID=8YFLogxK
U2 - 10.1109/RTAS.2016.7461337
DO - 10.1109/RTAS.2016.7461337
M3 - Conference contribution
AN - SCOPUS:84971320746
T3 - 2016 IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2016 - Proceedings
BT - 2016 IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2016 - Proceedings
PB - Institute of Electrical and Electronics Engineers Inc.
Y2 - 11 April 2016 through 14 April 2016
ER -