主 题: 信息科学系列报告（讨论班）—Dependable Model Driven Development of CPS: From Stateflow Simulation to Verified Implementation
报告人: 姜宇 (清华大学软件公司)
时 间: 2017-05-31 13:00-15:00
地 点: 理科1号楼1303
Abstract: Simulink is widely used for model-driven development (MDD) of cyber-physical systems. Typically, the Simulink based development starts with 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. Even the constructed Stateflow model and the generated code pass the validation of Simulink Design Verifier and Simulink Polyspace, respectively, the system may still fail due to some implicit bugs contained in the model and the generated code. In this paper, we present a novel 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 non-intrusive 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 offers 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 to the development of a typical cyber-physical systemtrain communication controller based on the International Electrotechnical Commission standard 61375. Experiments show that more ambiguousness in the standard are detected during Uppaal verification, and the errors have been confirmed. Furthermore, the verified implementation has been deployed on real trains.
