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

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.]]
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.]]
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.]]
12. Y. Gurevich. Sequential abstract state machines capture sequential algorithms. ACM Transactions on Computational Logic, 1(1):77--111, 2000.]]
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.]]
14. J. Jürjens. A UML statecharts semantics with message-passing. In SAC2002, ACM.]]
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.]]
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.]]
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.]]
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.]]