Abstract
UML is a widely used notation, and formalizing its semantics is an important issue. Here, we concentrate on formalizing UML state machines, used to express the dynamic behaviour of software systems. We propose a formal operational semantics covering all features of the latest version (2.4.1) of UML state machines specification. We use labelled transition systems as the semantic model, so as to use automatic verification techniques like model checking. Furthermore, our proposed semantics includes synchronous and asynchronous communications between state machines. We implement our approach in USM2C, a model checker supporting editing, simulation and automatic verification of UML state machines. Experiments show the effectiveness of our approach.
This work is supported by project 9.10.11 “Software Verification from Design to Implementation” of Programme Merlion (official collaborative grant co-funded by France and Singapore).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
OMG unified language superstructure specification (formal), Version 2.4.1 (August 06, 2011), http://www.omg.org/spec/UML/2.4.1/Superstructure/PDF/ .
USM 2 C, a UML state machines model checker (April 05, 2013), http://www.comp.nus.edu.sg/~lius87
André, É., Choppy, C., Klai, K.: Formalizing non-concurrent UML state machines using colored Petri nets. ACM SIGSOFT Software Engineering Notes 37(4), 1–8 (2012)
Beato, M.E., Barrio-Solórzano, M., Cuesta, C.E., Fuente, P.: UML automatic verification tool with formal methods. Elec. N. in Th. Computer Sc. 127(4), 3–16 (2005)
Börger, E., Cavarra, A., Riccobene, E.: On formalizing UML state machines using ASMs. Information Software Technology 46(5), 287 (2004)
Choppy, C., Klai, K., Zidani, H.: Formal verification of UML state diagrams: a Petri net based approach. ACM SIGSOFT Software Engineering Notes 36(1), 1–8 (2011)
Fecher, H., Schönborn, J.: UML 2.0 state machines: Complete formal semantics via core state machine. Formal Methods: Applications and Technology, 244–260 (2007)
Fecher, H., Schönborn, J., Kyas, M., de Roever, W.: 29 new unclarities in the semantics of UML 2.0 state machines. Formal Methods and Software Engineering, 52–65 (2005)
Gnesi, S., Latella, D., Massink, M.: Model checking UML statechart diagrams using JACK. In: HASE 1999, pp. 46–55 (1999)
Harel, D., Gery, E.: Executable object modeling with statecharts. IEEE Computer 30, 31–42 (1997)
Jin, Y., Esser, R., Janneck, J.: A method for describing the syntax and semantics of UML statecharts. Software and Systems Modeling 3(2), 150–163 (2004)
Jürjens, J.: A UML statecharts semantics with message-passing. In: Proceedings of the 2002 ACM Symposium on Applied Computing, pp. 1009–1013. ACM (2002)
Knapp, A., Merz, S.: Model checking and code generation for UML state machines and collaborations. In: Proc. 5th W. Tools System Design & Verif, vol. 11, pp. 59–64 (2002)
Knapp, A., Merz, S., Rauh, C.: Model checking - timed UML state machines and collaborations. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 395–416. Springer, Heidelberg (2002)
Kong, J., Zhang, K., Dong, J., Xu, D.: Specifying behavioral semantics of UML diagrams through graph transformations. Journal of Systems and Software 82(2), 292–306 (2009)
Lilius, J., Paltor, I.P.: vUML: A tool for verifying UML models, pp. 255–258 (1999)
Liu, S., Liu, Y., André, É., Choppy, C., Sun, J., Wadhwa, B., Dong, J.S.: A formal semantics for complete UML state machines with communications (report). Technical report, National University of Singapore (2013), http://www.comp.nus.edu.sg/~lius87/uml/techreport/uml_sm_semantics.pdf
Ng, M., Butler, M.: Towards formalizing UML state diagrams in CSP. In: SEFM 2003, p. 138 (2003)
Schönborn, J.: Formal semantics of UML 2.0 behavioral state machines. Technical report, Inst. Computer Science and Applied Mathematics, Christian-Albrechts-Univ. of Kiel (2005)
Shen, W., Compton, K., Huggins, J.: A toolset for supporting UML static and dynamic model checking. In: COMPSAC 2002, pp. 147–152 (2002)
Snook, C., Butler, M.: UML-B: Formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), 92–122 (2006)
Von Der Beeck, M.: A structured operational semantics for UML-statecharts. Software and Systems Modeling 1(2), 130–141 (2002)
Zhang, S., Liu, Y.: An automatic approach to model checking UML state machines. In: 4th Int. Conf. Secure Software Integration & Reliability etc (SSIRI-C), pp. 1–6. IEEE (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Liu, S. et al. (2013). A Formal Semantics for Complete UML State Machines with Communications. In: Johnsen, E.B., Petre, L. (eds) Integrated Formal Methods. IFM 2013. Lecture Notes in Computer Science, vol 7940. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38613-8_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-38613-8_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38612-1
Online ISBN: 978-3-642-38613-8
eBook Packages: Computer ScienceComputer Science (R0)