Abstract
The article presents a novel approach to model checking of UML activity diagrams (in version 2.x) for logic controller specification. A novel idea to design embedded systems by means of activity diagrams is introduced, using the previously proposed rule-based logical model suitable both for formal verification and logic synthesis. As the result implemented solution is consistent with the verified specification delivered in form of an user-friendly UML activity diagram. The idea is presented on a simple control process of two vehicles movement. Model checking technique is used to verify system model against behavioral properties expressed in temporal logic. In case of detected errors appropriate counterexamples are generated.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
OMG Unified Modeling Language (OMG UML) Superstructure ver. 2.4.1. Object Management Group (2011)
Grobelny, M., Grobelna, I., Adamski, M.: 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), Brno, pp. 109–114 (2012)
Grobelna, I., Grobelny, M., Adamski, M.: Petri Nets and activity diagrams in logic controller specification – transformation and verification. In: Proceedings of the 17th International Conference Mixed Design of Integrated Circuits and Systems, pp. 607–612 (2010)
Łabiak, G., Adamski, M., Doligalski, M., Tkacz, J., Bukowiec, A.: UML modelling in rigorous design methodology for discrete controllers. International Journal of Electronics and Telecommunications 58(1), 27–34 (2012)
David, R., Alla, H.: Discrete, Continuous, and Hybrid Petri Nets. Springer (2010)
Grobelna, I.: Formal verification of logic controller specification by means of model checking. Lecture Notes in Control and Computer Science, vol. 24. University of ZielonaGóra Press (2013)
Grobelna, I.: Formal verification of embedded logic controller specification with computer deduction in temporal logic. Przegląd Elektrotechniczny (12a), 40–43 (2011)
Kropf, T.: Introduction to Formal Hardware Verification. Springer (1999)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. The MIT Press (1999)
Emerson, E.A.: The Beginning of Model Checking: A Personal Perspective. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking: History, Achievements, Perspectives, pp. 27–45. Springer (2008)
Huth, M., Ryan, M.: Logic in Computer Science. Modelling and Reasoning about Systems. Cambridge University Press (2004)
Cavada, R., et al.: NuSMV 2.5 User Manual, http://nusmv.fbk.eu/
Ahrends, S.: Neue Ansätze für effizientes Rapid Prototyping von Embedded Systemen. In: Embedded Computing Conference (2008)
Wisniewski, R., Barkalov, A., Titarenko, L., Halang, W.A.: Design of microprogrammed controllers to be implemented in FPGAs. International Journal of Applied Mathematics and Computer Science 21(2), 401–412 (2011)
Lam, V.S.W.: A Formalism for Reasoning about UML Activity Diagrams. Nordic Journal of Computing 14(1), 43–64 (2007)
Achouri, A., Jemni Ben Ayed, L.: A Formal Semantic for UML 2.0 Activity Diagram based on Institution Theory. The International Journal of Soft Computing and Software Engineering (JSCSE) 3(3) (2013); Special Issue: The Proceedings of International Conference on Soft Computing and Software Engineering, USA
Eshuis, R., Wieringa, R.: A Formal Semantics for UML Activity Diagrams - Formalising Workflow Models. University of Twente, Centre for Telematics and Information Technology technical reports series (2001)
Andreu, D., Souquet, G., Gil, T.: Petri Net based rapid prototyping of digital complex system. In: IEEE Computer Society Annual Symposium on VLSI, pp. 405–410 (2008)
Adamski, M., Chodań, M.: Discreet control systems modelling using SFC nets. Wydawnictwo Politechniki Zielonogórskiej (2000) (in Polish)
Tkacz, J., Adamski, M.: Logic design of structured configurable controllers. In: IEEE 3rd International Conference on Networked Embedded Systems for Every Application (NESEA), pp. 1–6 (2012)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Grobelna, I., Grobelny, M., Adamski, M. (2014). Model Checking of UML Activity Diagrams in Logic Controllers Design. In: Zamojski, W., Mazurkiewicz, J., Sugier, J., Walkowiak, T., Kacprzyk, J. (eds) Proceedings of the Ninth International Conference on Dependability and Complex Systems DepCoS-RELCOMEX. June 30 – July 4, 2014, Brunów, Poland. Advances in Intelligent Systems and Computing, vol 286. Springer, Cham. https://doi.org/10.1007/978-3-319-07013-1_22
Download citation
DOI: https://doi.org/10.1007/978-3-319-07013-1_22
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-07012-4
Online ISBN: 978-3-319-07013-1
eBook Packages: EngineeringEngineering (R0)