More Web Proxy on the site http://driver.im/

article

Free access

A compositional approach to statecharts semantics

Authors:

Gerald Lüttgen,

Michael von der Beeck,

Rance CleavelandAuthors Info & Claims

ACM SIGSOFT Software Engineering Notes, Volume 25, Issue 6

Pages 120 - 129

https://doi.org/10.1145/357474.355062

Published: 01 November 2000 Publication History

Abstract

Statecharts is a visual language for specifying reactive system behavior. The formalism extends traditional finite-state machines with notions of hierarchy and concurrency, and it is used in many popular software design notations. A large part of the appeal of Statecharts derives from its basis in state machines, with their intuitive operational interpretation. The classical semantics of Statecharts, however, suffers from a serious defect; it is not compositional, meaning that the behavior of system descriptions cannot be inferred from the behavior of their subsystems. Compositionality is a prerequisite for exploiting the modular structure of Statecharts for simulation, verification, and code generation, and it also provides the necessary foundation for reusability.

This paper suggests a new compositional approach to formalizing Statecharts semantics as flattened labeled transition systems in which transitions represent system steps. The approach builds on ideas developed for timed process calculi and employs structural operational rules to define the transitions of a Statecharts expression in terms of the transitions of its subexpressions. It is first presented for a simple dialect of Statecharts, with respect to a variant of Pnueli and Shalev's semantics, and is illustrated by means of a small example. To demonstrate its flexibility, the proposed approach is then extended to deal with practically useful features available in many Statecharts variants, namely state references, history states, and priority concepts along state hierarchies.

References

[1]

R. Alur, S. Kannan, and M. Yannakakis. Communicating hierarchical state machines. In ICALP '99, volume 1644 of LNCS, pages 169-178. Springer-Verlag, 1999.]]

[2]

G. Berry and G. Gonthier. The ESTEREL synchronous programming language: Design, semantics, implementation. SCP, 19(2):87-152, 1992.]]

Digital Library

[3]

G. Botch, J. Rumbaugh, and I. Jacobson. The Unified Modeling Language User Guide. Addison Wesley, 1998.]]

Digital Library

[4]

R. Cleaveland and M. Hennessy. Priorities in process algebra. Inform. & Comp., 87(1/2):58-77, 1990.]]

Digital Library

[5]

R. Cleaveland, E. Madelaine, and S. Sims. Generating front-ends for verification tools. In TACAS "95, volume 1019 of LNCS, pages 153-173. Springer-Verlag, 1995.]]

[6]

R. Cleaveland and S. Sims. The NCSU CONCURRENCY WORKBENCH. In CAV '96, volume 1102 of LNCS, pages 394--397. Springer-Verlag, 1996.]]

[7]

W. Datum, B. Josko, H. Hungar, and A. Pnueli. A compositional real-time semantics of STATEMATE designs. In de Roever et al. {8}, pages 186--238.]]

Digital Library

[8]

W.-E de Roever, H. Langmaack, and A. Pnueli, editors. Compositionality: The Significant Difference, volume 1536 of LNCS. Springer-Verlag, 1997.]]

Digital Library

[9]

D. Harel. Statecharts: A visual formalism for complex systems. SCP, 8:231-274, 1987.]]

Digital Library

[10]

D. Harel and A. Naamad. The STATEMATE semantics of Statecharts. ACM Transactions on Software Engineering, 5(4):293-333, 1996.]]

Digital Library

[11]

D. Harel, A. Pnueli, J. Schmidt, and R. Sherman. On the formal semantics of Statecharts. In LICS "87, pages 56--64. IEEE Computer Society Press, 1987.]]

[12]

D. Harel and M. Politi. Modeling Reactive Systems with Statecharts: The STATEMATE Approach. McGraw Hill, 1998.]]

Digital Library

[13]

M. Hennessy and T. Regan. A process algebra for timed systems. Inform. & Comp., 117:221-239, 1995.]]

Digital Library

[14]

G. Holzmann. The model checker SPIN. 1EEE Trans. on Software Engineering, 23:279-295, 1997.]]

Digital Library

[15]

C. Huizing. Semantics of Reactive Systems: Comparison and Full Abstraction. Phi) thesis, Eindhoven University of Technology, 1991.]]

[16]

C. Huizing, R. Gerth, and W.-P. de Roever. Modeling Statecharts behavior in a fully abstract way. In CAAP '88, volume 299 of LNCS, pages 271-294. Springer-Verlag, 1988.]]

[17]

D. Latella, I. Majzik, and M. Massink. Towards a formal operational semantics of UML Statechart diagrams. In FMOODS '99. Kluwer, 1999.]]

Digital Library

[18]

E Levi. Verification of Temporal and Real-time Properties of Statecharts. PhD thesis, University of Pisa, 1997.]]

[19]

G. Lilttgen and M. Mender. Fully-abstract Statecharts semantics via intuitionistic Kripke models. In ICALP 2000, volume 1853 of LNCS, pages 163-174. Springer-Verlag, 2000.]]

Digital Library

[20]

G. Lttttgen, M. vonder Beeck, and R. Cleaveland. Statecharts via process algebra. In CONCUR '99, volume 1664 of LNCS, pages 399-414. Springer-Verlag, 1999.]]

[21]

A. Maggiolo-Schettini, A. Peron, and S. Tini. Equivalences of Statecharts. In CONCUR '96, volume 1119 of LNCS, pages 687-702. Springer-Verlag, 1996.]]

[22]

E Maraninchi. Operational and compositional semantics of synchronous automaton compositions. In CONCUR '92, volume 630 of LNCS, pages 550-564. Springer-Verlag, 1992.]]

[23]

E Maraninchi and N. Halbwachs. Compositional semantics of non-deterministic synchronous languages. In ESOP '96, volume 1058 of LNCS, pages 235-249. Springer-Verlag, 1996.]]

[24]

K. McMillan. Symbolic Model Checking: An Approach to the State-Explosion Problem. PhD thesis, Carnegie-Mellon University, 1992.]]

Digital Library

[25]

E. Mikk, Y. Lakhnech, C. Petersohn, and M. Siegel. On formal semantics of Statecharts as supported by STATEMATE. In Second BCS-FACS Northern Formal Methods Workshop. Springer-Verlag, 199%]]

[26]

E. Mikk, Y. Lakhnech, and M. Siegel. Hierarchical automata as model for Statecharts. In ASIAN '97, volume 1345 of LNCS. Springer-Verlag, 1997.]]

Digital Library

[27]

I. Paltor and J. Lilius. Formalising UML state machines for model checking. In UML '99, volume 1723 of LNCS, pages 430--445. Springer-Verlag, 1999.]]

[28]

G. Plotkin. A structural approach to operational semantics. Technical Report DAIMI-FN-19, Aarhus University, 1981.]]

[29]

A. Pnueli and M. Shalev. What is in a step: On the semantics of Statecharts. In TACS '91, volume 526 of LNCS, pages 244--264. Springer-Verlag, 1991.]]

[30]

P. Scholz. Design of Reactive Systems and Their Distributed Implementation with Statecharts. PhD thesis, Munich University of Technology, 1998.]]

[31]

B. Selic, G. Gullekson, and P. Ward. Real-time Object Oriented Modeling and Design. J. Wiley & Sons, 1994.]]

Digital Library

[32]

S. Seshia, R. Shyamasundar, A. Bhattacharjee, and S. Dhodapkar. A translation of Statecharts to ESTEREL. In FM '99, volume 1708 of LNCS, pages 983-1007. Springer-Verlag, 1999.]]

[33]

A. Uselton and S. Smolka. A compositional semantics for Statecharts using labeled transition systems. In CONCUR '94, volume 836 of LNCS, pages 2-17. Springer-Verlag, 1994.]]

[34]

A. Uselton and S. Smolka. A process-algebraic semantics for Statecharts via state refinement. In PROCOMET '94. North-Holland, 1994.]]

Digital Library

[35]

C. Verhoef. A congruence theorem for structured operational semantics with predicates and negative premises. Nordic J. of Comp., 2(2):274-302, 1995.]]

Digital Library

[36]

M. von der Beeck. A comparison of Statecharts variants. In FTRTFT '94, volume 863 of LNCS, pages 128-148. Springer-Verlag, 1994.]]

[37]

M. von der Beeck. A concise compositional Statecharts semantics definition. In FORTE/PSTV 2000. Kluwer, 2000. To appear.]]

Digital Library

Cited By

Uhrmacher AWilsdorf PKreikemeyer J(2024)Challenges and promises of self-adaptive simulation modelsSIMULATION10.1177/00375497241296878100:12(1281-1295)Online publication date: 2-Dec-2024
https://doi.org/10.1177/00375497241296878
Rączkowski DPokoniewski TBujak MOcypa ŁSzcześniak DSzurlej SŻuk P(2024)Optimization methods and procedures for DMLM parameters development process with digital tools assisted evaluation of the alloy metallography structure. based on the project RPMA.01.02.00-14-B479/18 from regionalny program Operacyjny Województwa MazowieckiegoXIV INTERNATIONAL CONFERENCE ELECTROMACHINING 202310.1063/5.0203808(020033)Online publication date: 2024
https://doi.org/10.1063/5.0203808
Ghzouli RBerger TJohnsen EWasowski ADragule S(2023)Behavior Trees and State Machines in Robotics ApplicationsIEEE Transactions on Software Engineering10.1109/TSE.2023.326908149:9(4243-4267)Online publication date: 21-Apr-2023
https://dl.acm.org/doi/10.1109/TSE.2023.3269081
Show More Cited By

Index Terms

A compositional approach to statecharts semantics
1. Software and its engineering
  1. Software creation and management
    1. Designing software
      1. Software implementation planning
        Software design techniques
    2. Software development process management
  2. Software notations and tools
    1. Formal language definitions
    2. System description languages
      1. Specification languages
2. Theory of computation
  1. Formal languages and automata theory
  2. Semantics and reasoning
    1. Program semantics
      1. Operational semantics

Recommendations

A compositional approach to statecharts semantics
SIGSOFT '00/FSE-8: Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications

Statecharts is a visual language for specifying reactive system behavior. The formalism extends traditional finite-state machines with notions of hierarchy and concurrency, and it is used in many popular software design notations. A large part of the ...
A UML statecharts semantics with message-passing
SAC '02: Proceedings of the 2002 ACM symposium on Applied computing

We give a formal semantics for one of the main UML diagram types for dynamical system behavior: statechart diagrams. This is the first semantics which explicitly models message-passing between different diagrams. It therefore lays a first foundation for ...
A method for describing the syntax and semantics of UML statecharts

In this article we present a method for describing the language of UML statecharts. Statecharts are syntactically defined as attributed graphs, with well-formedness rules specified by a set of first-order predicates over the abstract syntax of the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGSOFT Software Engineering Notes

ACM SIGSOFT Software Engineering Notes Volume 25, Issue 6

Nov. 2000

169 pages

ISSN:0163-5948

DOI:10.1145/357474

Editors:
Will Tracz
Lockheed Martin Federal systems, Owego, NY
,
David S. Rosenblum
Univ. of California, Irvine

Issue’s Table of Contents

SIGSOFT '00/FSE-8: Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications
November 2000
170 pages
ISBN:1581132050
DOI:10.1145/355045
Chairman:
John C. Knight
Univ of Virginia
,
Editor:
David S. Rosenblum
Univ of California, Irvine

Copyright © 2000 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 November 2000

Published in SIGSOFT Volume 25, Issue 6

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

36
Total Citations
View Citations
1,038
Total Downloads

Downloads (Last 12 months)92
Downloads (Last 6 weeks)11

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Uhrmacher AWilsdorf PKreikemeyer J(2024)Challenges and promises of self-adaptive simulation modelsSIMULATION10.1177/00375497241296878100:12(1281-1295)Online publication date: 2-Dec-2024
https://doi.org/10.1177/00375497241296878
Rączkowski DPokoniewski TBujak MOcypa ŁSzcześniak DSzurlej SŻuk P(2024)Optimization methods and procedures for DMLM parameters development process with digital tools assisted evaluation of the alloy metallography structure. based on the project RPMA.01.02.00-14-B479/18 from regionalny program Operacyjny Województwa MazowieckiegoXIV INTERNATIONAL CONFERENCE ELECTROMACHINING 202310.1063/5.0203808(020033)Online publication date: 2024
https://doi.org/10.1063/5.0203808
Ghzouli RBerger TJohnsen EWasowski ADragule S(2023)Behavior Trees and State Machines in Robotics ApplicationsIEEE Transactions on Software Engineering10.1109/TSE.2023.326908149:9(4243-4267)Online publication date: 21-Apr-2023
https://dl.acm.org/doi/10.1109/TSE.2023.3269081
Morris Wright KHoang TSnook CButler M(2023)Formal Language Semantics for Triggered Enable Statecharts with a Run-to-Completion SchedulingTheoretical Aspects of Computing – ICTAC 202310.1007/978-3-031-47963-2_12(178-195)Online publication date: 4-Dec-2023
https://dl.acm.org/doi/10.1007/978-3-031-47963-2_12
Liu HLiu JYin WSun HYang C(2022)Safety SysML: An Executable Safety-Critical Avionics Requirement Modeling Language2022 IEEE 22nd International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS57517.2022.00047(388-399)Online publication date: Dec-2022
https://doi.org/10.1109/QRS57517.2022.00047
de Haan GPost FGraham TCalvary GGray P(2009)StateStreamProceedings of the 1st ACM SIGCHI symposium on Engineering interactive computing systems10.1145/1570433.1570438(13-22)Online publication date: 15-Jul-2009
https://dl.acm.org/doi/10.1145/1570433.1570438
Hamon GRushby J(2004)An Operational Semantics for StateflowFundamental Approaches to Software Engineering10.1007/978-3-540-24721-0_17(229-243)Online publication date: 2004
https://doi.org/10.1007/978-3-540-24721-0_17
Dillon LStirewalt R(2003)Inference GraphsIEEE Transactions on Software Engineering10.1109/TSE.2003.117805229:2(133-150)Online publication date: 1-Feb-2003
https://dl.acm.org/doi/10.1109/TSE.2003.1178052
von der Beeck M(2001)Formalization of UML-Statecharts≪UML≫ 2001 — The Unified Modeling Language. Modeling Languages, Concepts, and Tools10.1007/3-540-45441-1_30(406-421)Online publication date: 17-Sep-2001
https://doi.org/10.1007/3-540-45441-1_30
Lüttgen G(2018)A Note on Refinement in Hierarchical Transition SystemsFormal Methods for Industrial Critical Systems10.1007/978-3-030-00244-2_14(211-222)Online publication date: 30-Aug-2018
https://doi.org/10.1007/978-3-030-00244-2_14
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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

Media

Figures

Other

Tables

View Issue’s Table of Contents