Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Invisible Formal Methods for Embedded Control Systems
Invisible Formal Methods for Embedded Control Systems
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.
@article{TiwariShankarRushby02,
TITLE = {Invisible formal methods for embedded control systems},
AUTHOR = {A. Tiwari and N. Shankar and J. Rushby},
JOURNAL = {Proceedings of the {IEEE}},
EDITOR = {Sastry, S. and Sztipanovits, J. and Bajcsy, R. and Gill, H.},
PAGES = "29--39",
VOLUME = 91,
NUMBER = 1,
MONTH = jan,
YEAR = 2003
}