Model Checking of UML Activity Diagrams Using a Rule-Based Logical Model

  • Iwona GrobelnaEmail author
  • Michał Grobelny
  • Marian Adamski
Part of the Studies in Systems, Decision and Control book series (SSDC, volume 45)


UML activity diagrams can be used as semi-formal specification of logic controller behavior. On the other hand, formal methods applied at any stage of system development allow increasing in the quality of final products. In the chapter use of the model checking technique to validate the specification against some specified requirements is described. The specification is initially expressed by means of UML activity diagrams and then is transformed to a rule-based logical model suitable both for verification purposes and for logical synthesis for FPGA devices.


Activity diagrams Formal methods Logic controller Model checking Specification Verification UML 


  1. 1.
    Ahrends, S. (2008). Neue Ansätze für effizientes Rapid Prototyping von Embedded Systemen. Embedded Computing Conference Google Scholar
  2. 2.
    Andreu, D., Souquet, G., & Gil, T. (2008). Petri net based rapid prototyping of digital complex system. In Proceedings of the 2008 IEEE Computer Society Annual Symposium on VLSI (pp. 405–410). Washington: IEEE Computer Society.Google Scholar
  3. 3.
    Clarke, E. M., Grumberg, O., & Peled, D. A. (1999). Model checking. Cambridge: The MIT Press.Google Scholar
  4. 4.
    David, R., & Alla, H. (2010). Discrete, continuous, and hybrid Petri nets (2nd ed.). Berlin: Springer.CrossRefGoogle Scholar
  5. 5.
    Doligalski, M., & Adamski, M (2013). UML state machine implementation inFPGA devices by means of dual model and Verilog. In 11th IEEE International Conference on Industrial Informatics - INDIN (pp. 177–184). Bochum, Germany. ISBN: 978-1-4799-0751-9Google Scholar
  6. 6.
    Emerson, E. A. (2008). The beginning of model checking: A personal perspective. In O. Grumberg & H. Veith (Eds.), 25 years of model checking (Vol. 5000, pp. 27–45). Lecture notes in computer science. Berlin: Springer.Google Scholar
  7. 7.
    Grobelna, I. (2011). Formal verification of embedded logic controller specification with computer deduction in temporal logic. Przeglad Elektrotechniczny, 87(12a), 47–50.Google Scholar
  8. 8.
    Grobelna, I. (2013). Formal verification of logic controller specification by means of model checking (Vol. 24). Lecture notes in control and computer science. Zielona Góra: University of Zielona Góra Press.Google Scholar
  9. 9.
    Grobelna, I., Grobelny, M., & Adamski, M. (2010). Petri nets and activity diagrams in logic controller specification - transformation and verification. In A. Napieralski (Ed.), 17th International Conference on Mixed Design of Integrated Circuits and Systems - MIXDES (pp. 607–612). Wroclaw.Google Scholar
  10. 10.
    Grobelny, M., Grobelna, I., Adamski, M. (2012). Hardware behavioural modelling, verification and synthesis with UML 2.x activity diagrams. In Proceedings of 11th IFAC/IEEE International Conference on Programmable Devices and Embedded Systems - PDeS 2012 (pp. 109–114). Brno.Google Scholar
  11. 11.
    Huth, M., & Ryan, M. (2004). Logic in computer science: Modelling and reasoning about systems. New York: Cambridge University Press.CrossRefGoogle Scholar
  12. 12.
    Kropf, T. (1999). Introduction to formal hardware verification: Methods and tools for designing correct circuits and systems (1st ed.). New York: Springer.CrossRefGoogle Scholar
  13. 13.
    Łabiak, G., Adamski, M., Tkacz, J., Doligalski, M., & Bukowiec, A. (2011). Role of UML modelling in discrete controller design. In D. Zydek & H. Selvaraj (Eds.), Proceedings of 21st International Conference on Systems Engineering ICSEng 2011 (pp. 480–481). Las Vegas, USA. University of Nevada, IEEE Computer Society. ISBN: 978-0-7695-4495-3.Google Scholar
  14. 14.
    OMG ( 2011). OMG Unified Modeling LanguageTM (OMG UML) Superstructure ver. 2.4.1. Object Management Group.Google Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Open Access This chapter is licensed under the terms of the Creative Commons Attribution-NonCommercial 2.5 International License (, which permits any noncommercial use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Authors and Affiliations

  • Iwona Grobelna
    • 1
    Email author
  • Michał Grobelny
    • 2
  • Marian Adamski
    • 3
  1. 1.Institute of Electrical EngineeringUniversity of Zielona GóraZielona GóraPoland
  2. 2.Department of Media and Information TechnologiesUniversity of Zielona GóraZielona GóraPoland
  3. 3.Institute of Metrology, Electronics and Computer ScienceUniversity of Zielona GóraZielona GóraPoland

Personalised recommendations