Paper Info
Title
Verifying simulink stateflow model: timed automata approach.
Abstract
Simulink Stateflow is widely used for the model-driven development of software. However, the increasing demand of rigorous verification for safety critical applications brings new challenge to the Simulink Stateflow because of the lack of formal semantics. In this paper, we present STU, a self-contained toolkit to bridge the Simulink Stateflow and a well-defined rigorous verification. The tool translates the Simulink Stateflow into the Uppaal timed automata for verification. Compared to existing work, more advanced and complex modeling features in Stateflow such as the event stack, conditional action and timer are supported. Then, with the strong verification power of Uppaal, we can not only find design defects that are missed by the Simulink Design Verifier, but also check more important temporal properties. The evaluation on artificial examples and real industrial applications demonstrates the effectiveness.
Year
DOI
Venue
2016
10.1145/2970276.2970293
ASE
Keywords
Field
DocType
Simulink Stateflow, Uppaal Timed Automaton, Verification
Synchronization,Programming language,Computer science,Automaton,Theoretical computer science,Software,Stateflow,Timer,Semantics,Semantics of logic,Embedded system
Conference
ISSN
ISBN
Citations 
1527-1366
978-1-5090-5571-5
8
PageRank 
References 
Authors
0.50
8
4
Name
Order
Citations
PageRank
Yixiao Yang1153.00
Yu Jiang234656.49
Ming Gu355474.82
Jia-guang Sun41807134.30