Operational Semantics for Stateflow
Grégoire Hamon and John Rushby
International Journal on Software Tools for Technology
Transfer (STTT), Volume 9, Numbers 5-6, October 2007; Special section
FASE'04/05, Pages 447--456.
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.
PDF
only
BibTeX Entry
@ARTICLE{Hamon&Rushby07:STTT,
AUTHOR = {Gr\'{e}goire Hamon and John Rushby},
TITLE = {An Operational Semantics for {Stateflow}},
JOURNAL = {International Journal on Software Tools for Technology Transfer (STTT)},
MONTH = oct,
YEAR = 2007,
VOLUME = 9,
NUMBER = {5--6},
PAGES = {447--456}
}
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