Formal modeling and validation of Stateflow diagrams
Stateflow is an industrial tool for modeling and simulating control systems in model-based development. In this paper, we present our latest work on automatic verification of Stateflow using model-checking techniques. We propose an approach to systematically translate Stateflow diagrams to a formal...
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | text |
| Language: | English |
| Published: |
Institutional Knowledge at Singapore Management University
2012
|
| Subjects: | |
| Online Access: | https://ink.library.smu.edu.sg/sis_research/5012 https://ink.library.smu.edu.sg/context/sis_research/article/6015/viewcontent/2012_Formal_Modeling_and_Validation_of_Stateflow_Diagrams.pdf |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Institution: | Singapore Management University |
| Language: | English |
| Summary: | Stateflow is an industrial tool for modeling and simulating control systems in model-based development. In this paper, we present our latest work on automatic verification of Stateflow using model-checking techniques. We propose an approach to systematically translate Stateflow diagrams to a formal modeling language called CSP# by precisely following Stateflow’s execution semantics, which is described by examples. A translator is developed inside the Process Analysis Toolkit (PAT) model checker to automate this process with the support of various Stateflow advanced modeling features. Formal analysis can be conducted on the transformed CSP# with PAT’s simulation and model-checking power. Using our approach, we can not only detect bugs in Stateflow diagrams, but also discover subtle semantics flaws in Stateflow user’s guide and demo cases. |
|---|