Problem hierarchii w transformacji diagramów aktywności UML 2.x do sieci Petriego sterowania

• Autorzy: Grobelny M. , Grobelna I.

Warianty tytułu

EN

Hierarchy problem in transformation of UML 2.x Activity Diagrams into Control Interpreted Petri Nets

• Języki publikacji: PL

Abstrakty

PL

Proces specyfikacji zachowania odgrywa istotną rolę z powodu określania na tym etapie cech i sposobu funkcjonowania sterownika logicznego. W artykule omówione zostały dwie metody graficznego specyfikowania zachowania sterowników logicznych - diagramy aktywności języka UML 2.x oraz sieci Petriego sterowania. Zaproponowana została metoda transformacji hierarchicznych diagramów aktywności do hierarchicznych sieci Petriego. Dzięki przedstawionej metodzie możliwe jest połączenie zalet obu typów graficznego opisu specyfikacji urządzeń. Dodatkowo, zaproponowana została metoda formalnej weryfikacji hierarchicznej formy specyfikacji umożliwiająca wykrycie potencjalnych błędów na tym wczesnym etapie projektu.

EN

Behavior specification is one of the most important steps in embedded systems design. It plays a significant role because system properties and functionality are specified in this phase. There exist some techniques which can be helpful for a designer. In the paper two methods for graphical specification of logic controller behavioral specification [1, 2, 6], namely UML 2.x activity diagrams [10] and control Petri nets [11], are considered. A novel transformation method for transformation of hierarchical activity diagrams into hierarchical Petri nets is proposed. The presented method allows combining the advantages of both types of graphical system specification. Additionally, a formal verification method for hierarchical specification form is proposed. It enables detecting potential errors at early stage of system development. Hierarchical form of specification is commonly used in design process. Activity diagrams can include complex actions (Fig. 1) which describe some subprocesses. Petri nets also support hierarchy, but it can be realized in two different forms [9] - as macroplaces or macrotransitions (Fig. 2). According to the transformation method from [3, 8], actions in activity diagrams are interpreted as transitions in Petri net. In hierarchical processes by means of Petri nets two elements, macrotransitions (Fig. 3) and macroplaces (Fig. 4), have to be considered. The macroplace (Fig. 5a) can be surrounded by two transitions (Fig. 5b), decomposed (Fig. 5c), and finally compressed to macrotransition (Fig. 5d), then transformed into complex activity in an UML 2.x activity diagram (Fig. 5e). Verification of both considered specification forms [3] allows comparing two versions of the same behavior description. The model checking technique [4] can be used to verify the whole system or a part of it. Partial verification can be used for hierarchical specifications, as the verification process can be performed step by step (Fig. 6).

Słowa kluczowe

PL

diagramy aktywności UML; sieci Petriego sterowania; modelowanie behawioralne; metody formalnej weryfikacji

EN

UML activity diagrams; control Petri nets; behavioral modelling; formal verification methods

• Wydawca: Wydawnictwo PAK
• Czasopismo: Pomiary Automatyka Kontrola
• Rocznik: 2011
• Tom: R. 57, nr 7
• Strony: 729--732
• Opis fizyczny: Bibliogr. 11 poz., rys.

Twórcy

autor

Grobelny M.

autor

Grobelna I.

• Uniwersytet Zielonogórski, ul. Podgórna 50, 65-246 Zielona Góra,

Bibliografia

• [1] Adamski M., Chodań M.: Modelowanie układów sterowania dyskretnego z wykorzystaniem sieci SFC, Zielona Góra: Wydawnictwo Politechniki Zielonogórskiej, 2000.
• [2] Adamski M., Karatkevich A., Węgrzyn M. (ed.): Design of embedded control systems, Springer (USA), 2005.
• [3] Gomes L., Barros J. P., Costa A.: Modeling formalisms for embedded system design, Embedded Systems Handbook, Taylor & Francis Group, LLC, 2006.
• [4] David R., Alla H.: Petri Nets & Grafcet. Tools for modeling discrete event systems, Prentice Hall, 1992.
• [5] Wrycza S., Marcinkowski B., Wyrzykowski K.: Język UML 2.0 w modelowaniu systemów informatycznych, Gliwice: Helion, 2005.
• [6] 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, ss. 27-45.
• [7] Węgrzyn A.: Symboliczna analiza układów sterowania binarnego z wykorzystaniem wybranych metod analizy sieci Petriego, Zielona Góra: Oficyna wydawnicza UZ, 2003.
• [8] Grobelna I., Grobelny M., Adamski M.: Petri Nets and activity diagrams in logic controller specification - transformation and verification, Mixed Design of Integrated Circuits and Systems - MIXDES 2010, Wrocław, Polska, 2010, ss. 607-612.
• [9] Grobelny M., Grobelna I.: Diagramy aktywności języka UML i sieci Petriego w systemach sterowania binarnego - od transformacji do weryfikacji, Pomiary Automatyka Kontrola, nr 10, ss. 1154-1158, 2010.
• [10] 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, ss. 11 200.
• [11] Basile F., Chiachio P., Del Grosso D.: Modelling automation systems by UML and Petri Nets, Proceedings of the 9th International Workshop on Disscreet Event Systems, Goteborg, Sweden, 2008, ss. 308-313.