@inproceedings{301,
  author = {Daniel Balasubramanian and Corina Pasareanu and Michael Whalen and Gabor Karsai and Michael Lowry},
  title = {Polyglot: Modeling and Analysis for Multiple Statechart Formalisms},
  abstract = {In large programs such as NASA Exploration, multiple systems that interact via safety-critical protocols are already designed with different Statechart variants.  To verify these safety-critical systems, a unified framework is needed based on a formal semantics that captures the variants of Statecharts.  We describe Polyglot, a unified 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 different variants, and addresses previous limitations.  Polyglot has been integrated with the Java Jathfinder verification tool-set, providing analysis and test-case generation capabilities.  We describe the application of this unified framework to the analysis of NASA/JPL's MER Arbiter whose interacting components were modeled using multiple Statechart formalisms.},
  year = {2011},
  journal = {International Symposium on Software Testing and Analysis (ISSTA)},
  month = {07/2011},
  address = {Toronto, Canada},
}