Model Checking of UML Activity Diagrams Using a Rule-Based Logical Model
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.
KeywordsActivity diagrams Formal methods Logic controller Model checking Specification Verification UML
- 1.Ahrends, S. (2008). Neue Ansätze für effizientes Rapid Prototyping von Embedded Systemen. Embedded Computing Conference Google Scholar
- 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.Clarke, E. M., Grumberg, O., & Peled, D. A. (1999). Model checking. Cambridge: The MIT Press.Google Scholar
- 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.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.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.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.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.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
- 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.OMG ( 2011). OMG Unified Modeling LanguageTM (OMG UML) Superstructure ver. 2.4.1. Object Management Group.Google Scholar
Open Access This chapter is licensed under the terms of the Creative Commons Attribution-NonCommercial 2.5 International License (http://creativecommons.org/licenses/by-nc/2.5/), 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.