A Formal Semantics for Complete UML State Machines with Communications
作者： Shuang Liu , Yang Liu , Étienne André , Christine Choppy , Jun Sun
DOI: 10.1007/978-3-642-38613-8_23
关键词:
摘要: UML is a widely used notation, and formalizing its semantics an important issue. Here, we concentrate on state machines, to express the dynamic behaviour of software systems. We propose formal operational covering all features latest version (2.4.1) machines specification. use labelled transition systems as semantic model, so automatic verification techniques like model checking. Furthermore, our proposed includes synchronous asynchronous communications between machines. implement approach in USM2C, checker supporting editing, simulation Experiments show effectiveness approach.
springer.com
smu.edu.sg
univ-paris13.fr
core.ac.uk 参考文章(22)
Harald Fecher, Jens Schönborn, UML 2.0 State Machines: Complete Formal Semantics Via core state machine Formal Methods: Applications and Technology. pp. 244- 260 ,(2007) , 10.1007/978-3-540-70952-7_16
Stephan Merz, Alexander Knapp, Model Checking and Code Generation for UML State Machines and Collaborations ,(2002)
Harald Fecher, Jens Schönborn, Marcel Kyas, Willem-Paul de Roever, 29 new unclarities in the semantics of UML 2.0 state machines formal methods. pp. 52- 65 ,(2005) , 10.1007/11576280_5
S. Gnesi, D. Latella, M. Massink, Model checking UML Statechart diagrams using JACK high-assurance systems engineering. pp. 46- 55 ,(1999) , 10.1109/HASE.1999.809474
Alexander Knapp, Stephan Merz, Christopher Rauh, Model Checking - Timed UML State Machines and Collaborations Lecture Notes in Computer Science. pp. 395- 416 ,(2002) , 10.1007/3-540-45739-9_23
Formal Techniques in Real-Time and Fault-Tolerant Systems Kluwer Academic Publishers. ,(1993) , 10.1007/978-1-4615-3220-0
M. Encarnación Beato, Manuel Barrio-Solórzano, Carlos E. Cuesta, Pablo de la Fuente, UML Automatic Verification Tool with Formal Methods Electronic Notes in Theoretical Computer Science. ,vol. 127, pp. 3- 16 ,(2005) , 10.1016/J.ENTCS.2004.10.024
Yan Jin, Robert Esser, Jörn W. Janneck, A method for describing the syntax and semantics of UML statecharts Software and Systems Modeling. ,vol. 3, pp. 150- 163 ,(2004) , 10.1007/S10270-003-0046-6
Colin Snook, Michael Butler, UML-B ACM Transactions on Software Engineering and Methodology. ,vol. 15, pp. 92- 122 ,(2006) , 10.1145/1125808.1125811
Étienne André, Christine Choppy, Kais Klai, Formalizing non-concurrent UML state machines using colored petri nets ACM Sigsoft Software Engineering Notes. ,vol. 37, pp. 1- 8 ,(2012) , 10.1145/2237796.2237819