An Operational Semantics for Stateflow

Grégoire Hamon and John Rushby

Presented at Fundamental Approaches to Software Engineering (FASE) Barcelona, Spain, March 2004.
Appears in Springer Verlag LNCS 2984, pp. 229-243. Copyright Springer Verlag LNCS

Abstract

We present a formal operational semantics for Stateflow, the graphical statecharts-like language of the Matlab/Simulink tool suite that is widely used in model-based development of embedded systems. Stateflow has many tricky features but our operational treatment yields a surprisingly simple semantics for the subset that is generally recommended for industrial applications. We have validated our semantics by developing an interpreter that allows us to compare its behavior against the Matlab simulator. We have used the semantics as a foundation for developing prototype tools for formal analysis of Stateflow designs.

gzipped postscript, or plain postscript or PDF or crude ascii (for your Palm Pilot)

*NOTE* An updated journal version is available.

BibTeX Entry

@INPROCEEDINGS{Hamon&Rushby:FASE04,
	AUTHOR = {Gr\'{e}goire Hamon and John Rushby},
	TITLE = {An Operational Semantics for {Stateflow}},
	BOOKTITLE = {Fundamental Approaches to Software Engineering:
		7th International Conference {(FASE)}},
	EDITOR ={M. Wermelinger and T. Margaria-Steffen},
	PAGES = {229--243},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 2984,
	ADDRESS = {Barcelona, Spain},
	DATE = apr,
	YEAR = 2004
}
Having trouble reading our papers?
Return to John Rushby's bibliography page
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page