Publication Type

Journal Article

Version

publishedVersion

Publication Date

1-2012

Abstract

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.

Keywords

Model-based development, Transformation Validation, Model checking, Stateflow

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

International Journal on Software Tools for Technology Transfer

Volume

14

First Page

653

Last Page

671

ISSN

1433-2779

Identifier

10.1007/s10009-012-0235-0

Publisher

Springer Verlag (Germany)

Additional URL

https://doi.org/10.1007/s10009-012-0235-0

Download

Share

COinS