Skip to main content
SpringerLink
Log in

Formal Verification of UML State Machine Diagrams Using Petri Nets

  • Conference paper
  • First Online:
Networked Systems (NETYS 2019)

Part of the book series: Lecture Notes in Computer Science ((LNCCN,volume 11704))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

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

    Google Scholar 

  2. Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541–580 (1989)

    Article  Google Scholar 

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

    Google Scholar 

  4. Budinsky, F., Steinberg, D., Ellersick, R., Grose, T.J., Merks, E.: Eclipse Modeling Framework: A Developer’s Guide. Addison-Wesley Professional, Boston (2004)

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  6. David, A., Möller, M.O., Yi, W.: Formal verification of UML statecharts with real-time extensions. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 218–232. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45923-5_15

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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

    Google Scholar 

  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

    Google Scholar 

  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

    Google Scholar 

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

    Article  Google Scholar 

  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)

    Google Scholar 

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

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LRIT - CNRST URAC No. 29, Faculty of Sciences, Rabat IT Center, Mohammed V University, Rabat, Morocco

    Achraf Lyazidi & Salma Mouline

Authors
  1. Achraf Lyazidi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Salma Mouline
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Achraf Lyazidi .

Editor information

Editors and Affiliations

  1. Uppsala University, Uppsala, Uppsala Län, Sweden

    Mohamed Faouzi Atig

  2. Augusta University, Augusta, GA, USA

    Alexander A. Schwarzmann

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Lyazidi, A., Mouline, S. (2019). Formal Verification of UML State Machine Diagrams Using Petri Nets. In: Atig, M., Schwarzmann, A. (eds) Networked Systems. NETYS 2019. Lecture Notes in Computer Science(), vol 11704. Springer, Cham. https://doi.org/10.1007/978-3-030-31277-0_5

Download citation

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

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-31276-3

  • Online ISBN: 978-3-030-31277-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation