University of Minnesota
Software Engineering Center

You are here

Integrating Statechart Components in Polyglot

Date of Publication: 
April 2012
Associated Research Groups: 
Publication Files: 
Statecharts is a model-based formalism for simulating and analyzing reactive systems. In our previous work, we developed Polyglot, a unified framework for analyzing different semantic variants of Statechart models. However, for systems containing communicating, asynchronous components deployed on a distributed platform, additional features not inherent to the basic Statecharts paradigm are needed. These include a connector mechanism for communication, a scheduling framework for sequencing the execution of individual components, and a method for specifying verification properties spanning multiple components. This paper describes the addition of these features to Polyglot, along with an example NASA case study using these new features. Furthermore, the paper describes on-going work on modeling Plexil execution plans with Polyglot, which enables the study of interaction issues for future manned and unmanned missions.
Proceedings of the Fourth NASA Formal Methods Symposium, Norfolk, VA, April 3-5, 2012
@inproceedings{NFM2012:BaPaBiPrKaLoWh, author = {Daniel Balasubramanian and Corina S. P{\va}s{\va}reanu and Jason Biatek and Thomas Pressburger and Gabor Karsai and Michael R. Lowry and Michael W. Whalen}, title = {Integrating Statechart Components in Polyglot}, booktitle = {Proceedings of the 4th NASA Formal Methods Symposium (NFM 2012)}, volume = {7226}, editor = {Alwyn E. Goodloe and Suzette Person}, location = {Norfolk, VA, USA}, publisher = {Springer-Verlag}, address = {Berlin, Heidelberg}, pages = {267--272}, month = {April}, year = {2012} }