research-article

Polyglot: modeling and analysis for multiple Statechart formalisms

Authors:

Daniel Balasubramanian,

Corina S. Păsăreanu,

Michael W. Whalen,

Michael LowryAuthors Info & Claims

ISSTA '11: Proceedings of the 2011 International Symposium on Software Testing and Analysis

Pages 45 - 55

https://doi.org/10.1145/2001420.2001427

Published: 17 July 2011 Publication History

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 State-chart 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 Pathfinder 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.

References

[1]

Java pathfinder tool-set. http://babelfish.arc.nasa.gov/trac/jpf, 2011.

[2]

C. André. Computing synccharts reactions. Electron. Notes Theoretical Computer Science, 88:3--19, 2004.

Digital Library

[3]

D. Balasubramanian, G. Pap, H. Nine, G. Karsai, M. Lowry, C. S. Păsăreanu, and T. Pressburger. Rapid property specification and checking for model-based formalisms. In IEEE International Symposium on Rapid System Prototyping (RSP'2011), 2011.

[4]

E. Börger, A. Cavarra, and E. Riccobene. Modeling the dynamics of uml state machines. In ASM '00: Proceedings of the International Workshop on Abstract State Machines, Theory and Applications, pages 223--241, London, UK, 2000. Springer-Verlag.

Digital Library

[5]

A. Childs, J. Greenwald, V. P. Ranganath, X. Deng, M. B. Dwyer, J. Hatcliff, G. Jung, P. Shanti, and G. Singh. Cadena: An integrated development environment for analysis, synthesis, and verification of component-based systems. In FASE, pages 160--164, 2004.

[6]

K. Compton, J. Huggins, and W. Shen. A semantic model for the state machine in the unified modeling language. In In Proceeding of Dynamic Behavior in UML Models: Semantic Questions, UML 2000 workshop, pages 25--31. Springer Verlag, 2000.

[7]

M. L. Crane and J. Dingel. Uml vs. classical vs. rhapsody statecharts: Not all models are created equal. 2005.

[8]

J. Eker, J. Janneck, E. A. Lee, J. Liu, X. Liu, J. Ludvig, S. Sachs, and Y. Xiong. Taming heterogeneity - the ptolemy approach. Proceedings of the IEEE, 91(1):127--144, January 2003.

[9]

S. Esmaeilsabzali and N. A. Day. Prescriptive semantics for big-step modelling languages. In 13th International Conference on Fundamentals of Software Engineering, March 2010.

Digital Library

[10]

S. Esmaeilsabzali, N. A. Day, J. M. Atlee, and J. Niu. Big-step semantics. Technical Report CS-2009-05, David R. Chariton School of Computer Science, University of Waterloo, Ontario, Canada N2l 3G1, February 2009.

[11]

M. Gogolla and F. Parisi-Presicce. State diagrams in uml: A formal semantics using graph transformations. In PSMT'98 Workshop on Precise Semantics for Modeling Techniques. Technische Universitat Munchen, 1998.

[12]

O. M. Group. Unified Modeling LanguageTM (OMG UML), Superstructure Version 2.2. Object Management Group, February 2009.

[13]

M. Hamilton. The heart and soul of apollo: Doing it right the first time. In Proc. 7th International Military and Aerospace Programmable Logic Devices (MAPLD) Conference, 2004.

[14]

G. Hamon. A denotational semantics for stateflow. In Proceedings of the Embedded Systems Software Conference, Jersey City, New Jersey, September 2005. ACM.

Digital Library

[15]

G. Hamon and J. Rushby. An operational semantics for stateflow. In Proc. Fundamental Approaches to Software Engineering (FASE) Conference, pages 229--243, Barcelona, Spain, March 2004. Springer Verlag (LNCS 2984).

[16]

D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3):231--274, June 1987.

Digital Library

[17]

D. Harel and H. Kugler. The rhapsody semantics of statecharts (or, on the executable core of the uml). In In Integration of Software Specification Techniques for Application in Engineering, number 3147 in Lecture Notes in Computer Science, pages 325--354. Springer, 2001.

[18]

M. P. E. Heimdahl and N. G. Leveson. Completeness and consistency in hierarchical state-base requirements. IEEE Trans. on Software Engineering, 22(6):363--377, June 1996.

Digital Library

[19]

J. C. King. Symbolic execution and program testing. Commun. ACM, 19(7):385--394, 1976.

Digital Library

[20]

Á. Lédeczi, A. Bakay, M. Maroti, P. Völgyesi, G. Nordstrom, J. Sprinkle, and G. Karsai. Composing domain-specific design environments. IEEE Computer, 34(11):44--51, 2001.

Digital Library

[21]

Mathworks Inc. Stateflow product web site. http://www.mathworks.com.

[22]

S. P. Miller, M. W. Whalen, and D. D. Cofer. Software model checking takes off. Commun. ACM, 53(2):58--64, 2010.

Digital Library

[23]

M. Pezzè and M. Young. Constructing multi-formalism state-space analysis tools: Using rules to specify dynamic semantics of models. In ICSE, pages 239--249, 1997.

Digital Library

[24]

G. D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, September 1981.

[25]

C. S. Păsăreanu and D. Giannakopoulou. Towards a compositional SPIN. In Proc. SPIN Workshop, 2006.

Digital Library

[26]

C. S. Păsăreanu and N. Rungta. Symbolic PathFinder: Symbolic execution of Java bytecode. In Proceedings of ASE, pages 179--180, 2010.

Digital Library

[27]

C. S. Păsăreanu, J. Schumann, P. Mehlitz, M. Lowry, G. Karsai, H. Nine, and S. Neema. Model based analysis and test generation for flight software. In SMC-IT, 2009.

Digital Library

[28]

G. Reggio, E. Astesiano, C. Choppy, and H. Hussmann. Analysing uml active classes and associated state machines - a lightweight formal approach. In Fundamental Approaches to Software Engineering, LNCS 1783, pages 127--146. Springer, 2000.

Digital Library

[29]

V. Verma, T. Estlin, A. Jonsson, C. S. Păsăreanu, and R. Simmons. Plan execution interchange language (plexil) for command execution. In Proceedings of iSAIRAS, 2005.

[30]

M. von der Beeck. A structured operational semantics for uml-statecharts. Software and Systems Modeling, 1:130--141, 2002. 10.1007/s10270-002-0012-8.

[31]

M. von der Beek. A comparison of statecharts variants. Formal Techniques in Real-Time and Fault-Tolerant Systems, 526, 1994.

Digital Library

[32]

M. W. Whalen. A formal semantics for RSML ^-e. Master's thesis, University of Minnesota, May 2000.

[33]

M. W. Whalen. A parametric structural operational semantics for Stateflow, UML statecharts, and Rhapsody. Technical Report 2010-1, CSE Dept., University of Minnesota, August 2010.

Cited By

Kurian EBraione PBriola DD’Avino DModonato MDenaro G(2023)Automated Test Case Generation for Safety-Critical Software in Scade2023 IEEE/ACM 45th International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP)10.1109/ICSE-SEIP58684.2023.00049(483-494)Online publication date: May-2023
https://doi.org/10.1109/ICSE-SEIP58684.2023.00049
Kurian EBriola DBraione PDenaro G(2023)Automatically generating test cases for safety-critical software via symbolic executionJournal of Systems and Software10.1016/j.jss.2023.111629199:COnline publication date: 1-May-2023
https://dl.acm.org/doi/10.1016/j.jss.2023.111629
Ahmadi RDingel JDumas MPfahl DApel SRusso A(2019)Concolic testing for models of state-based systemsProceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3338906.3338908(4-15)Online publication date: 12-Aug-2019
https://dl.acm.org/doi/10.1145/3338906.3338908
Show More Cited By

Recommendations

Integrating statechart components in polyglot
NFM'12: Proceedings of the 4th international conference on NASA Formal Methods

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 ...
STATEMATE: A Working Environment for the Development of Complex Reactive Systems

STATEMATE is a set of tools, with a heavy graphical orientation, intended for the specification, analysis, design, and documentation of large and complex reactive systems. It enables a user to prepare, analyze, and debug diagrammatic, yet precise, ...
Polyglot: systematic analysis for multiple statechart formalisms
TACAS'13: Proceedings of the 19th international conference on Tools and Algorithms for the Construction and Analysis of Systems

Polyglot is a tool for the systematic analysis of systems integrated from components built using multiple Statechart formalisms. In Polyglot, Statechart models are translated into a common Java representation with pluggable semantics for different ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ISSTA '11: Proceedings of the 2011 International Symposium on Software Testing and Analysis

July 2011

394 pages

ISBN:9781450305624

DOI:10.1145/2001420

General Chair:
Matthew Dwyer
University of Nebraska
,
Program Chair:
Frank Tip
IBM T.J. Watson Research Center

Copyright © 2011 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

In-Cooperation

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 July 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ISSTA '11

Sponsor:

SIGSOFT

ISSTA '11: International Symposium on Software Testing and Analysis

July 17 - 21, 2011

Ontario, Toronto, Canada

Acceptance Rates

Overall Acceptance Rate 58 of 213 submissions, 27%

Upcoming Conference

ISSTA '25

Sponsor:
sigsoft

34th ACM SIGSOFT International Symposium on Software Testing and Analysis

June 25 - 28, 2025

Trondheim , Norway

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

30
Total Citations
View Citations
273
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kurian EBraione PBriola DD’Avino DModonato MDenaro G(2023)Automated Test Case Generation for Safety-Critical Software in Scade2023 IEEE/ACM 45th International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP)10.1109/ICSE-SEIP58684.2023.00049(483-494)Online publication date: May-2023
https://doi.org/10.1109/ICSE-SEIP58684.2023.00049
Kurian EBriola DBraione PDenaro G(2023)Automatically generating test cases for safety-critical software via symbolic executionJournal of Systems and Software10.1016/j.jss.2023.111629199:COnline publication date: 1-May-2023
https://dl.acm.org/doi/10.1016/j.jss.2023.111629
Ahmadi RDingel JDumas MPfahl DApel SRusso A(2019)Concolic testing for models of state-based systemsProceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3338906.3338908(4-15)Online publication date: 12-Aug-2019
https://dl.acm.org/doi/10.1145/3338906.3338908
Matinnejad RNejati SBriand LBruckmann T(2019)Test Generation and Test Prioritization for Simulink Models with Dynamic BehaviorIEEE Transactions on Software Engineering10.1109/TSE.2018.281148945:9(919-944)Online publication date: 1-Sep-2019
https://doi.org/10.1109/TSE.2018.2811489
Ahmadi RJahed KDingel JZimmermann TLawall JMarinov D(2019)mCUTEProceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE.2019.00132(1182-1185)Online publication date: 10-Nov-2019
https://dl.acm.org/doi/10.1109/ASE.2019.00132
Yang GQiu RKhurshid SPăsăreanu CWen J(2019)A synergistic approach to improving symbolic execution using test rangesInnovations in Systems and Software Engineering10.1007/s11334-019-00331-9Online publication date: 9-Apr-2019
https://doi.org/10.1007/s11334-019-00331-9
Liu BNejati SLucia Briand L(2019)Effective fault localization of automotive Simulink modelsEmpirical Software Engineering10.1007/s10664-018-9611-z24:1(444-490)Online publication date: 1-Feb-2019
https://dl.acm.org/doi/10.1007/s10664-018-9611-z
Bak SBeg OBogomolov SJohnson TNguyen LSchilling C(2019)Hybrid automataInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-017-0458-121:1(87-104)Online publication date: 1-Feb-2019
https://dl.acm.org/doi/10.1007/s10009-017-0458-1
Bhattacharyya SEskridge TNeogi NCarvalho MStafford M(2018)Formal Assurance for Cooperative Intelligent Autonomous AgentsNASA Formal Methods10.1007/978-3-319-77935-5_2(20-36)Online publication date: 11-Mar-2018
https://doi.org/10.1007/978-3-319-77935-5_2
Liu BLucia Nejati SBriand L(2017)Improving fault localization for Simulink models using search-based testing and prediction models2017 IEEE 24th International Conference on Software Analysis, Evolution and Reengineering (SANER)10.1109/SANER.2017.7884636(359-370)Online publication date: Feb-2017
https://doi.org/10.1109/SANER.2017.7884636
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents