Article

Modeling the meaning of transitions from and to concurrent states in UML state machines

Authors:

Alessandra Cavarra,

Elvinia RiccobeneAuthors Info & Claims

SAC '03: Proceedings of the 2003 ACM symposium on Applied computing

Pages 1086 - 1091

https://doi.org/10.1145/952532.952745

Published: 09 March 2003 Publication History

Abstract

This paper completes the ASM models developed for UML state machines in [4, 5] providing new submachines covering also transitions from and to concurrent states in the context of event deferring and run-to-completion. Due to the modular structure of the earlier ASM models for UML state diagrams, these new submachines can be inserted there as components. The modular treatment explicitly reflects the corresponding intended "semantic variation points" of UML, thus allowing to adapt definitions given in this paper to possibly changing standardization decisions.

References

[1]

OMG Unified Modeling Languages Specification, version 1.4, 2001.]]

[2]

A. Blass and Y. Gurevich. Abstract State Machines Capture Parallel Algorithms. (MSR-TR-2001-117).]]

[3]

E. Börger. High level system design and analysis using abstract state machines. In D. Hutter et al., editor, FM 98, number 1641 in LNCS. 1999.]]

[4]

E. Börger, A. Cavarra, and E. Riccobene. Modeling the Dynamics of UML State Machines. In Y. Gurevich et al., editor, Abstract State Machines. Theory and Applications, volume 1912 of LNCS. Springer.]]

Digital Library

[5]

E. Börger, A. Cavarra, and E. Riccobene. A precise semantics of UML State Machines: making semantic variation points and ambiguities explicit. In Proc. SFEDL02 - ETAPS 2002, 2002.]]

[6]

E. Börger and J. Schmid. Composition and submachine concepts for sequential asms. In P. Clote et al., editor, Computer Science Logic (Gurevich Festschrift), number 1862 in LNCS.]]

[7]

A. Cavarra. Applying Abstract State Machines to Formalize and Integrate the UML Lightweight Method. PhD thesis, University, of Catania, Italy, 2000.]]

[8]

K. Compton, J. Huggins, and W. Shen. A semantic model for the state machine in the Unified Modeling Language. In Dynamic Behavior in UML Models: Semantic Questions UML 2000 workshop, 2000.]]

[9]

S. Gnesi, D. Latella, and M. Massink. Model checking UML statechart diagrams using JACK. In R. Paul and C. Meadows, editors, Fourth IEEE International Symposium on High Assurance Systems Engineering.]]

Digital Library

[10]

M. Gogolla and F. P. Presicce. State diagrams in UML: A formal semantics using graph transformations. In M. Broy et al., editor, Proc. PSMT'98. TUM-I9803.]]

[11]

Y. Gurevich. Evolving Algebras 1993: Lipari Guide. In E. Börger, editor, Specification and Validation Methods, pages 9--36. Oxford University Press, 1995.]]

Digital Library

[12]

Y. Gurevich. Sequential abstract state machines capture sequential algorithms. ACM Transactions on Computational Logic, 1(1):77--111, 2000.]]

Digital Library

[13]

Y. Jin, R. Esser, and J. W. Janneck. Describing the Syntax and Semantics of UML Statecharts in a Heterogeneous Modelling Environment. In Diagrams 2002, volume 2317. LNAI, 2002.]]

Digital Library

[14]

J. Jürjens. A UML statecharts semantics with message-passing. In SAC2002, ACM.]]

Digital Library

[15]

J. Jürjens. Formal Semantics for Interacting UML subsystems. In FMOODS 2002. Kluwer, 2002.]]

[16]

S. Kuske. A formal semantics of UML State Machines based on structured graph transformation. In M. Gogolla and C. Kobryn, editors, Proc. UML 2001, volume 2185 of LNCS.]]

Digital Library

[17]

D. Latella, I. Majzik, and M. Massink. Automatic verification of a behavioural subset of UML diagrams using the SPIN model-checker. FAC99, 11(6).]]

[18]

D. Latella, I. Majzik, and M. Massink. Towards a formal operational semantics of UML statechart diagrams. In Proc. FMOODS99. Chapmann and Hall.]]

Digital Library

[19]

I. Paltor and J. Lilius. Formalising UML state machines for model checking. In R. France et al., editor, UML99, volume 1723 of LNCS. Springer.]]

[20]

G. Reggio, E. Astesiano, C. Choppy, and H. Hussmann. Analysing UML Active Classes and Associated State Machines -- A Lightweight Formal Approach. In T. Maibaum, editor, Proc. FASE 2000, volume 1783 of LNCS. Springer, 2000.]]

Digital Library

[21]

T. Schfer, A. Knapp, and S. Merz. Model Checking UML State Machines and Collaborations. Electronic Notes in Theoretical Computer Science, 47:1--13, 2001.]]

[22]

M. von der Beeck. Formalization of UML-Statecharts. In M. Gogolla et al., UML2001, Vol. 2185 of LNCS.]]

Digital Library

Cited By

Ferreira DLima L(2024)A CSP Semantics for UML State Machines Aiming at Hidden Formal Methods VerificationFormal Methods: Foundations and Applications10.1007/978-3-031-78116-2_4(49-67)Online publication date: 29-Nov-2024
https://doi.org/10.1007/978-3-031-78116-2_4
André ÉLiu SLiu YChoppy CSun JDong J(2023)Formalizing UML State Machines for Automated Verification – A SurveyACM Computing Surveys10.1145/357982155:13s(1-47)Online publication date: 13-Jul-2023
https://dl.acm.org/doi/10.1145/3579821
Lund MRefsdal AStølen K(2010)4 Semantics of UML Models for Dynamic BehaviorModel-Based Engineering of Embedded Real-Time Systems10.1007/978-3-642-16277-0_4(77-103)Online publication date: 2010
https://doi.org/10.1007/978-3-642-16277-0_4
Show More Cited By

Recommendations

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 ...
UML with meaning: executable modeling in foundational UML and the Alf action language
HILT '14: Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology

To most in the software community, "modeling" is drawing pictures, something much different than "coding". While programming languages must be specified precisely enough to be executable, this has not necessarily been the case for modeling languages. ...
A framework to simulate UML models: moving from a semi-formal to a formal environment
SAC '04: Proceedings of the 2004 ACM symposium on Applied computing

This paper presents a simulation framework for UML models based upon a mapping schema of UML metamodel elements into Abstract State Machines (ASMs). Structural model elements are translated into an ASM vocabulary as collections of domains and functions, ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

SAC '03: Proceedings of the 2003 ACM symposium on Applied computing

March 2003

1268 pages

ISBN:1581136242

DOI:10.1145/952532

Conference Chair:
Gary B. Lamont
Air Force Institute of Technology
,
Program Chairs:
Hisham Haddad
Kennesaw State University
,
George A. Papadopoulos
University of Cyprus, Cyprus
,
Publications Chair:
Brajendra Panda
University of Arkansas

Copyright © 2003 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

SIGAPP: ACM Special Interest Group on Applied Computing

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 March 2003

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

SAC03

Sponsor:

SIGAPP

SAC03: ACM Symposium on Applied Computing

March 9 - 12, 2003

Florida, Melbourne

Acceptance Rates

Overall Acceptance Rate 1,650 of 6,669 submissions, 25%

Upcoming Conference

SAC '25

Sponsor:
sigapp

The 40th ACM/SIGAPP Symposium on Applied Computing

March 31 - April 4, 2025

Catania , Italy

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
634
Total Downloads

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

Reflects downloads up to 25 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ferreira DLima L(2024)A CSP Semantics for UML State Machines Aiming at Hidden Formal Methods VerificationFormal Methods: Foundations and Applications10.1007/978-3-031-78116-2_4(49-67)Online publication date: 29-Nov-2024
https://doi.org/10.1007/978-3-031-78116-2_4
André ÉLiu SLiu YChoppy CSun JDong J(2023)Formalizing UML State Machines for Automated Verification – A SurveyACM Computing Surveys10.1145/357982155:13s(1-47)Online publication date: 13-Jul-2023
https://dl.acm.org/doi/10.1145/3579821
Lund MRefsdal AStølen K(2010)4 Semantics of UML Models for Dynamic BehaviorModel-Based Engineering of Embedded Real-Time Systems10.1007/978-3-642-16277-0_4(77-103)Online publication date: 2010
https://doi.org/10.1007/978-3-642-16277-0_4
Schönborn JKyas M(2010)Refinement Patterns for Hierarchical UML State MachinesFundamentals of Software Engineering10.1007/978-3-642-11623-0_22(371-386)Online publication date: 2010
https://doi.org/10.1007/978-3-642-11623-0_22
Lund MRefsdal AStølen K(2007)Semantics of UML models for dynamic behaviorProceedings of the 2007 International Dagstuhl conference on Model-based engineering of embedded real-time systems10.5555/1927558.1927564(77-103)Online publication date: 4-Nov-2007
https://dl.acm.org/doi/10.5555/1927558.1927564
Börger ECavarra ARiccobene E(2004)On formalizing UML state machines using ASMsInformation and Software Technology10.1016/j.infsof.2003.09.00946:5(287-292)Online publication date: Apr-2004
https://doi.org/10.1016/j.infsof.2003.09.009
Jin YEsser RJanneck J(2004)A method for describing the syntax and semantics of UML statechartsSoftware and Systems Modeling (SoSyM)10.1007/s10270-003-0046-63:2(150-163)Online publication date: 1-May-2004
https://dl.acm.org/doi/10.1007/s10270-003-0046-6
Stevens P(2003)UML and concurrencyProceedings of the abstract state machines 10th international conference on Advances in theory and practice10.5555/1754749.1754758(151-166)Online publication date: 3-Mar-2003
https://dl.acm.org/doi/10.5555/1754749.1754758
Stevens P(2003)UML and ConcurrencyAbstract State Machines 200310.1007/3-540-36498-6_8(151-166)Online publication date: 14-Mar-2003
https://doi.org/10.1007/3-540-36498-6_8

View Options

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