Article

Formal Verification of UML State Machine Diagrams Using Petri Nets

Authors:

Achraf Lyazidi,

Salma MoulineAuthors Info & Claims

Networked Systems: 7th International Conference, NETYS 2019, Marrakech, Morocco, June 19–21, 2019, Revised Selected Papers

Pages 67 - 74

https://doi.org/10.1007/978-3-030-31277-0_5

Published: 19 June 2019 Publication History

Abstract

UML State Machine diagrams are widely used for behavioral modeling. They describe all of the possible states of a system and show its lifetime behavior. Nevertheless, they lack of semantics. A State Machine diagram may be interpreted in different manners that can lead to unwanted situations. In this paper, we propose a formal verification phase for UML State Machine diagrams using a formal language. The aim is to ensure UML State Machine diagrams properties to designers and to highlight errors. Petri nets, a formal notation for concurrent systems, are suitable for modeling systems behavior and they are well supported by analysis tools. Based on Model-Driven Engineering, we define a transformation from UML State Machine diagrams to Petri nets. The resulting Petri nets models are formally verified regarding properties. We also define a post-interpretation of the verification results in terms of UML State Machine diagrams.

References

[1]

Drusinsky D Modeling and Verification Using UML Statecharts: A Working Guide to Reactive System Design, Runtime Monitoring and Execution-Based Model Checking 2011 Amsterdam Elsevier

[2]

Murata T Petri nets: properties, analysis and applications Proc. IEEE 1989 77 4 541-580

[3]

Berthomieu, B., Vernadat, F.: Time Petri nets analysis with TINA. In: QEST, vol. 6, pp. 123–124, September 2006

[4]

Budinsky F, Steinberg D, Ellersick R, Grose TJ, and Merks E Eclipse Modeling Framework: A Developer’s Guide 2004 Boston Addison-Wesley Professional

[5]

Jouault F, Allilaire F, Bézivin J, and Kurtev I ATL: a model transformation tool Sci. Comput. Program. 2008 72 1–2 31-39

[6]

David A, Möller MO, and Yi W Kutsche R-D and Weber H Formal verification of UML statecharts with real-time extensions Fundamental Approaches to Software Engineering 2002 Heidelberg Springer 218-232

[7]

Latella D, Majzik I, and Massink M Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker Formal Aspects Comput. 1999 11 6 637-664

[8]

Knapp, A., Merz, S.: Model checking and code generation for UML state machines and collaborations. In: Proceedings 5th Wsh. Tools for System Design and Verification, pp. 59–64 (2002)

[9]

Jussila, T., Dubrovin, J., Junttila, T., Latvala, T., Porres, I., Linz, J.K.U.: Model checking dynamic and hierarchical UML state machines. In: Proceedings MoDeV2a: Model Development, Validation and Verification, Genova, Italy, pp. 94–110 (2006)

[10]

Bernardi, S., Donatelli, S., Merseguer, J.: From UML sequence diagrams and statecharts to analysable Petri net models. In: Proceedings of the 3rd International Workshop on Software and Performance, Rome, Italy, pp. 35–45. ACM, July 2002

[11]

Saldhana, J., Shatz, S. M.: UML diagrams to object Petri net models: an approach for modeling and analysis. In: International Conference on Software Engineering and Knowledge Engineering, Chicago, IL, USA, pp. 103–110, July 2000

[12]

Hu, Z., Shatz, S.M.: Mapping UML diagrams to a Petri net notation for system simulation. In: International Conference on Software Engineering and Knowledge Engineering, Anbert, Canada, pp. 213–219, June 2004

[13]

André É, Choppy C, and Klai K Formalizing non-concurrent UML state machines using colored Petri nets SIGSOFT Softw. Eng. Notes 2012 37 4 1-8

[14]

André, E., Benmoussa, M.M., Choppy, C.: Translating UML state machines to coloured Petri nets using Acceleo: a report. In: Proceedings of the Third International Workshop on Engineering Safety and Security Systems, Singapore, pp. 1–7 (2014)

[15]

Choppy C, Klai K, and Zidani H Formal verification of UML state diagrams: a Petri net based approach SIGSOFT Softw. Eng. Notes 2011 36 1 1-8

Cited By

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
Stramaglia AKeiren J(2022)Formal Verification of an Industrial UML-like Model using mCRL2Formal Methods for Industrial Critical Systems10.1007/978-3-031-15008-1_7(86-102)Online publication date: 14-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-15008-1_7

Index Terms

Formal Verification of UML State Machine Diagrams Using Petri Nets
1. Software and its engineering
2. Theory of computation
  1. Semantics and reasoning

Index terms have been assigned to the content through auto-classification.

Recommendations

Formal verification of UML state diagrams: a petri net based approach

In spite of its informal semantics and of some ambiguities, UML is a widespread modelling language used in both industry and academia. On the other hand, Petri nets are a mathematical modelling language with a formal semantics and are well suited for ...
Automatic Model Transformation from UML Sequence Diagrams to Coloured Petri Nets
MODELSWARD 2018: Proceedings of the 6th International Conference on Model-Driven Engineering and Software Development

UML Sequence Diagrams are used in different domains for specifying the required behaviour of software-based

systems. However, the created diagrams are often used only as documentation, and not as a basis for

generating subsequent lifecycle artifacts or ...
Using MDE for the formal verification of embedded systems modeled by UML sequence diagrams
SBCCI '09: Proceedings of the 22nd Annual Symposium on Integrated Circuits and System Design: Chip on the Dunes

This work presents a formal verification methodology that adopts concepts from Model Driven Engineering (MDE) for the automatic generation of a network of timed automata from the functional specification of an embedded application described using UML ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

Networked Systems: 7th International Conference, NETYS 2019, Marrakech, Morocco, June 19–21, 2019, Revised Selected Papers

Jun 2019

397 pages

ISBN:978-3-030-31276-3

DOI:10.1007/978-3-030-31277-0

Editors:
Mohamed Faouzi Atig
Uppsala University, Uppsala, Uppsala Län, Sweden
,
Alexander A. Schwarzmann
Augusta University, Augusta, GA, USA

© Springer Nature Switzerland AG 2019.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 19 June 2019

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 20 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

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
Stramaglia AKeiren J(2022)Formal Verification of an Industrial UML-like Model using mCRL2Formal Methods for Industrial Critical Systems10.1007/978-3-031-15008-1_7(86-102)Online publication date: 14-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-15008-1_7

View Options

View options

Media

Figures

Other

Tables

View Table of Contents