Polyglot: Modeling and Analysis for Multiple Statechart Formalisms

Thumbnail Image

View/Download File

Persistent link to this item

View Statistics

Journal Title

Journal ISSN

Volume Title


Polyglot: Modeling and Analysis for Multiple Statechart Formalisms

Published Date







In large programs such as NASA Exploration, multiple systems that interact via safety-critical protocols are already designed with dierent Statechart variants. To verify these safety-critical systems, a unied framework is needed based on a formal semantics that captures the variants of Statecharts. We describe Polyglot, a unied framework for the analysis of models described using multiple Statechart formalisms. In this framework, Statechart models are translated into Java and analyzed using pluggable semantics for different variants operating in a polymorphic execution environment. The framework has been built on the basis of a parametric formal semantics that captures the common core of Statecharts with extensions for dierent variants, and addresses previous limitations. Polyglot has been integrated with the Java Pathnder verication tool-set, providing analysis and test-case generation capabilities. We describe the application of this unied framework to the analysis of NASA/JPL's MER Arbiter whose interacting components were modeled using multiple Statechart formalisms.



Associated research group: Critical Systems Research Group

Related to



Series/Report Number

Funding information

Isbn identifier

Doi identifier

Previously Published Citation

Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), Toronto, Ontario, Canada, July 17-21, 2011.

Suggested citation

Balasubramanian, Daniel; Păsăreanu, Corina; Whalen, Michael; Karsai, Gabor; Lowry, Michael. (2011). Polyglot: Modeling and Analysis for Multiple Statechart Formalisms. Retrieved from the University Digital Conservancy, https://hdl.handle.net/11299/217399.

Content distributed via the University Digital Conservancy may be subject to additional license and use restrictions applied by the depositor. By using these files, users agree to the Terms of Use. Materials in the UDC may contain content that is disturbing and/or harmful. For more information, please see our statement on harmful content in digital repositories.