Diagramy aktywności języka UML i sieci Petriego w systemach sterowania binarnego - od transformacji do weryfikacji

• Autorzy: Grobelny M. , Grobelna I.

Warianty tytułu

EN

UML activity diagrams and Petri nets in binary control systems - from transformation to verification

• Języki publikacji: PL

Abstrakty

PL

Język UML jest technologią powszechnie stosowaną w świecie naukowym oraz w przemyśle. Sieci Petriego są modelem matematycznym ogólnego zastosowania ugruntowanym od wielu lat. Obie te techniki doskonale nadają się do specyfikacji procesów sterowania. Jednakże jako odmienne, każda z nich posiada unikatowe właściwości. Technika weryfikacji modelowej jest jedną z metod formalnej weryfikacji specyfikacji pozwalającą na zdiagnozowanie błędów w specyfikacji wymagań albo w opisie modelu. Artykuł przedstawia metodę transformacji pomiędzy obiema wymienionymi technikami specyfikacji w celu formalnej weryfikacji projektu sterowania opisanego w języku UML.

EN

Unified Modeling Language (UML) [1-3, 5, 6-8] is commonly used in scientific and industrial world. Petri nets [9] are mathematical model used for a long period of time. Both techniques are well suited for control processes specification. However, they are quite different. Each technique has its own unique properties. Model checking technique [14-17] is one of formal verification methods [18] for specifications. It allows detecting errors either in requirements specification or in model description. The paper presents the method for transformation between both mentioned specification techniques - from UML activity diagram (Fig. 1) to Petri net (Fig. 4), using some defined rules [10, 11]. Mapping of particular elements is presented in Table 1. Petri net after direct transformation may include redundant places which can be after-wards removed. Then, it is possible to formally verify control process described in UML. The proposed model checker tool is NuSMV [20]. NuSMV (Fig. 5) compares model description (Fig. 6 - 8) and requirements (Fig. 9) which have to be fulfilled. The requirements are defined using temporal logic. If a specified requirement may not be fulfilled, appropriate counterexamples are generated (Fig. 10) which allow detecting an error source. Then, the specification can be corrected and model checking process can start again, sometimes including only the particular part of a designed system.

Słowa kluczowe

PL

diagramy aktywności UML; sieci Petriego; weryfikacja modelowa

EN

UML activity diagrams; Petri nets; model checking

• Wydawca: Wydawnictwo PAK
• Czasopismo: Pomiary Automatyka Kontrola
• Rocznik: 2010
• Tom: R. 56, nr 10
• Strony: 1154--1158
• Opis fizyczny: Bibliogr. 21 poz., rys., tab., wzor

Twórcy

autor

Grobelny M.

autor

Grobelna I.

• Uniwersytet Zielonogórski, Instytut Informatyki i Elektroniki, ul. Szafrana 2, 65-246 Zielona Góra,

Bibliografia

• [1] Graessle P., Baumann H., Baumann P.: UML 2.0 w akcji. Przewodnik oparty na projektach, Helion 2006, str. 17-38.
• [2] Miles R., Hamilton K.: UML 2.0. Wprowadzenie, Helion 2007.
• [3] Wrycza S., Marcinkowski B., Wyrzykowski K.: UML 2.0 w modelowaniu systemów informatycznych, Helion 2005.
• [4] Oficjalna strona internetowa konsorcjum Object Management Group, http://www.omg.org
• [5] Adamski M. A., Karatkevich A., Węgrzyn M. (ed.): Design of embedded control systems, Springer Science+Business Media, Inc., 2005.
• [6] Yen-Liang C., Sammy C., Chyun-Chyi C., Irene C.: Workflow Process Definition and Their Applications in e-Commerce, IEEE 2000, str. 193-200.
• [7] Eshuis R., Wieringa R.: A Comparison of Petri Net and Activity Diagram Variants, Proc. of 2nd Int. Coll. on Petri Net Technologies for Modelling Communication Based Systems 2001, str. 93-104.
• [8] Schattkowsky T.: UML 2.0 - Overview and Perspectives in SoC Design, Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE’05).
• [9] David R., Alla H.: Petri Nets & Grafcet. Tools for modeling discrete event systems, Prentice Hall 1992.
• [10] Grobelny M.: Transformacja diagramów aktywności UML 2.0 do sieci Petriego w systemach sterowania binarnego, Pomiary, Automatyka, Kontrola, 2009, nr 7, str. 498-500.
• [11] Yao S., Shatz S. M.: Consistency Checking of UML Dynamic Model Based on Petri Net Techniques, Proceedings of the 15th International Conference on Computing, IEEE 2006.
• [12] Staines T. S.: Intuitive Mapping of UML 2 Activity Diagrams into Fundamental Modeling Concept Petri Net Diagrams and Colored Petri Nets, 15th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems, 2008, str. 191-200.
• [13] Tričković I.: Formalizing activity diagram of UML by Petri nets, Novi Sad J. Math, Vol. 30, No 3, 2000, pp. 161-171.
• [14] Clarke E. M., Burch J. R., Grumberg O., Long D. E., McMillan K. L.: Automatic verification of sequential circuit designs, Phil. Trans. R. Soc. Lond. A (1992) 339, str. 105-120.
• [15] Clarke E. M., Emerson E. A., Sistla A. P.: Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems, Vol. 8, No 2, April 1986, str. 244-263.
• [16] Emerson E. A.: The Beginning of Model Checking: A Personal Perspective, Lecture Notes in Computer Science, 25 Years of Model Checking: History, Achievements, Perspectives, 2008, str. 27-45.
• [17] Rice M. V., Vardi M. Y.: Branching vs. Linear Time: Final Showdown, Proceedings of the 2001 Conference on Tools and Algorithms for the Construction and Analysis of Systems, TA-CAS 2001, LNCS Volume 2031, Springer-Verlag 2001, str. 1-22.
• [18] Clarke E. M., Wing J. M. et al.: Formal methods: State of the Art and Future Directions, ACM Computing Surveys, Vol. 28, No 4, 1996.
• [19] Crane M. L., Dingel J.: Towards a UML virtual machine: implementing an interpreter for UML 2 actions and activities, Proceedings of the 2008 conference of the center for advanced studies on collaborative research, IEEE 2008.
• [20] Cavada R. et al. : NuSMV 2.4 User Manual, http://nusmv.irst.itc.it, 2005.
• [21] Grobelna I.: Formalna analiza interpretowanych algorytmicznych maszyn stanów ASM z wykorzystaniem narzędzia model checker, Metody Informatyki Stosowanej nr 3/2008, Tom 16, str. 107-124.