Formal Semantics and Analysis Methods for Simulink Stateflow Models

Ashish Tiwari

Unpublished report.


Embedded control systems typically comprise continuous control laws combined with discrete mode logic. The Simulink graphical environment of MathWorks' tool suite is a popular choice for modeling and designing embedded controllers. Mode logic in Simulink models is described in terms of hierarchical state machines specified in a variant of Statecharts called Stateflow. The semantics of Stateflow is quite complex and it is valuable if these designs can be formally analyzed for both early error detection and positive assurance. It is important that formal analysis should be unobtrusive and acceptable to engineering practice. We motivate a methodology called ``invisible formal methods'' that provides a graded sequence of formal analysis technologies ranging from extended typechecking, through approximation and abstraction, to model checking and theorem proving. As an instance of invisible formal methods, we describe the formal semantics of a fragment of Stateflow based on a modular representation called {\em communicating pushdown automata}. We show how this semantics can be used to analyze simple properties of Stateflow models.


BibTeX Entry

     author = "A. Tiwari",
     year = 2002,
     institution = "SRI International",
     title = "Formal semantics and analysis methods for {S}imulink {S}tateflow models",
     note = "{\tt\-$\sim$tiwari/\-stateflow.html}"

Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page