SKLCS Seminar
Title: Formal Verification of Simulink/Stateflow Diagrams
Speaker: Shuling Wang (Institute of Software, CAS)
Time: 15:00, 29th September 2015
Venue: Seminar Room (334), Level 3, Building 5, Institute of Software,
Chinese Academy of Sciences.
Abstract.
Simulink is an industrial de-facto standard for building executable
models of control systems and their environments. Stateflow is a
toolbox used to model reactive systems via hierarchical statecharts
within a Simulink model, extending Simulink's scope to event-driven
and hybrid forms of embedded control. In safety-critical control
systems, exhaustive coverage of system dynamics by formal
verification would be desirable, being based on a formal semantics
of combined Simulink/Stateflow graphical models.
In our previous work, we addressed the problem of formal verification of pure
Simulink diagrams via an encoding into HCSP, a formal modelling
language encoding hybrid system dynamics by means of an extension of
CSP. In this talk, we present our recent work that extends the approach to
cover Simulink models containing Stateflow components also. The transformation
from Simulink/Stateflow to HCSP is fully automatic, and the formal
verification of the encoding is supported by a Hybrid Hoare Logic
(HHL) prover based on Isabelle/HOL. We demonstrate our approach by
a real world case study originating from the Chinese High-speed
Train Control System (CTCS-3).
This is a joint work with Naijun Zhan, Liang Zou, and Martin Fraenzle.
Biography:
Dr. Shuling Wang is currently an assistant professor of the State Key Lab.
of Computer Science, Institute of Software, Chinese Academy of Sciences.
Before that, she received her Ph.D. degree from Peking University in 2008,
and she was a postdoc of UNU-IIST and ISCAS from 2008 to 2010 and from
2010 to 2012 respectively.
