Formal Verification of UML State Machine Diagrams Using Petri Nets

  • Achraf LyazidiEmail author
  • Salma Mouline
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11704)


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.


UML State Machine diagrams Petri nets Formal verification Model transformation Model-Driven Engineering 


  1. 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. 2.
    Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541–580 (1989)CrossRefGoogle Scholar
  3. 3.
    Berthomieu, B., Vernadat, F.: Time Petri nets analysis with TINA. In: QEST, vol. 6, pp. 123–124, September 2006Google Scholar
  4. 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. 5.
    Jouault, F., Allilaire, F., Bézivin, J., Kurtev, I.: ATL: a model transformation tool. Sci. Comput. Program. 72(1–2), 31–39 (2008)MathSciNetCrossRefGoogle Scholar
  6. 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). Scholar
  7. 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)CrossRefGoogle Scholar
  8. 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. 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. 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 2002Google Scholar
  11. 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 2000Google Scholar
  12. 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 2004Google Scholar
  13. 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)CrossRefGoogle Scholar
  14. 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. 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)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.LRIT - CNRST URAC No. 29, Faculty of Sciences, Rabat IT CenterMohammed V UniversityRabatMorocco

Personalised recommendations