Formal Semantics and Analysis Methods for Simulink Stateflow Models
Ashish Tiwari
Unpublished report.
Abstract
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.
pdf
BibTeX Entry
@techreport{StateflowSemantics,
author = "A. Tiwari",
year = 2002,
institution = "SRI International",
title = "Formal semantics and analysis methods for {S}imulink {S}tateflow models",
note = "{\tt http://www.csl.sri.com/\-$\sim$tiwari/\-stateflow.html}"
}
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page