Invisible Formal Methods for Embedded Control Systems

Ashish Tiwari, N. Shankar, and John Rushby

© Copyright Proceedings of the IEEE . This paper appears in the Special issue on Modeling and Design of Embedded Software.

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


@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
}
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page