Petri nets and activity diagrams in logic controller specification – transformation and verification

• Autorzy: Grobelna I. , Grobelny M. , Adamski M.

Warianty tytułu

PL

Sieci petriego i diagramy aktywności w specyfikacji sterowników logicznych – transformacja i weryfikacja

• Języki publikacji: EN

Abstrakty

EN

The paper presents formal verification method of logic controller specification taking into account user-specified properties. Logic controller specification may be expressed as Petri net or UML 2.0 Activity Diagram. Activity Diagrams seem to be more user-friendly and easy-understanding that Petri nets. Specification in form of activity diagram may afterwards be transformed into Petri net, which may then be formally verified and used to automatically generate implementation (code). A new transformation method dedicated for event-driven systems is proposed. Verification process is executed automatically by the NuSMV model checker tool. Model description based on specification and properties list is being built. Model description derived from Petri net is presented in RTL-level and easy to synthesize as reconfigurable logic controller or PLC. Properties are defined using temporal logic. In model checking process, verification tool checks whether requirements are satisfied in attached system model. If this is not the case, appropriate counterexamples are generated.

PL

Praca prezentuje metodę formalnej weryfikacji specyfikacji sterownika logicznego uwzględniającą właściwości podane przez użytkownika. Specyfikacja sterownika logicznego może być przedstawiona m.in. w postaci sieci Petriego lub diagramu aktywności języka UML. Diagramy aktywności wydają się być bardziej przyjazne i zrozumiałe dla użytkownika niż sieci Petriego. Specyfikacja w postaci diagramu aktywności może zostać przekształcona do sieci Petriego, która następnie może być formalnie zweryfikowana i wykorzystana do automatycznej generacji implementacji (kodu). Węzły diagramu aktywności konsekwentnie interpretowane są jako tranzycje sieci Petriego, w odróżnieniu od klasycznego podejścia (w starszych wersjach UML) gdzie odwzorowywało się je jako miejsca sieci Petriego. Proces weryfikacji wykonywany jest automatycznie przez narzędzia weryfikacji modelowej. Tworzony jest opis modelu bazujący na specyfikacji oraz lista wymagań. Nowatorskim podejściem jest przedstawienie sieci Petriego na poziomie RTL w taki sposób, że łatwo jest przeprowadzić syntezę logiczną sieci w postaci współbieżnego rekonfigurowalnego sterownika logicznego lub sterownika PLC bez konieczności przekształcania modelu. Wymagania określone są przy użyciu logiki temporalnej. W procesie weryfikacji modelowej narzędzie weryfikujące NuSMV sprawdza, czy model systemu spełnia stawiane mu wymagania. Jeżeli tak nie jest, generowany jest odpowiedni kontrprzykład.

Słowa kluczowe

EN

formal verification; logic controller; model checking; Petri nets; UML Activity; Diagrams

PL

formalna weryfikacja; sterownik logiczny; weryfikacja modelowa; sieci Petriego; diagramy aktywności UML

• Wydawca: Wydawnictwa Uczelniane Politechniki Bydgoskiej im. Jana i Jędrzeja Śniadeckich
• Czasopismo: Zeszyty Naukowe. Telekomunikacja i Elektronika / Uniwersytet Technologiczno-Przyrodniczy w Bydgoszczy
• Rocznik: 2010
• Tom: z. 13
• Strony: 79--91
• Opis fizyczny: Bibliogr. 23 poz., rys.

Twórcy

autor

Grobelna I.

• nstitute of Computer Eng. And Electronics University of Zielona Góra Zielona Góra, Poland

autor

Grobelny M.

autor

Adamski M.

Bibliografia

• [1] Andreu D., Souquet G., Gil T., 2008. Petri Net based rapid prototyping of digital complex system, Symposium on VLSI, IEEE Computer Society Annual, pp. 405- 410.
• [2] Adamski M., 2001. A rigorous design methodology for reprogrammable logic controllers, The International Workshop on Discrete-Event System Design, DESDes'01, Przytok, Poland.
• [3] Adamski M., Chodań M., 2000. Modelowanie układów sterowania dyskretnego z wykorzystaniem sieci SFC, Wydawnictwo Politechniki Zielonogórskiej, Zielona Góra (in Polish).
• [4] Adamski M., Karatkevich A., Węgrzyn M. (ed.), 2005. Design of embedded control systems, Springer (USA).
• [5] Ben-Ari M., 2005. Logika matematyczna w informatyce. Klasyka informatyki, Wydawnictwa Naukowo-Techniczne, Warszawa (in Polish).
• [6] Cavada R. et al. NuSMV 2.4 User Manual, downloaded from http://nusmv.fbk.eu/
• [7] Clarke E.M., Wind J.M. et al, 1996. Formal methods: State of the Art and Future Directions, ACM Computing Surveys, Vol. 28, No. 4.
• [8] David R., Alla H., 1992. Petri Nets & Grafcet. Tools for modelling discrete event systems, Prentice Hall.
• [9] Eshuis R., 2006. Symbolic Model Checking of UML Activity Diagrams, ACM Transactions on Software Engineering and Methodology, Vol. 15, No. 1, pp. 1-38.
• [10] Eshuis R., Wieringa R., 2001. A Comparison of Petri Net and Activity Diagram Variants, Proc. of 2nd Int. Coll. on Petri Net Technologies for Modelling Communication Based Systems, pp. 93-104.
• [11] Frey G., Litz L., 1998. Verification and Validation of Control Algorithms by Coupling of Interpreted Petri Nets, Proceedings of the IEEE SMC'98, Vol. 1, pp. 7-12.
• [12] Gomes L., Barros J.P., Costa A., 2006. Modeling Formalisms for Embedded System Design, Embedded Systems Handbook, Taylor & Francis Group, LLC.
• [13] Grobelna I., 2008. Formalna analiza interpretowanych algorytmicznych maszyn stanów ASM z wykorzystaniem narzędzia model checker, Metody Informatyki Stosowanej nr 3, Tom 16, pp. 107-124 (in Polish).
• [14] Grobelna I., 2008. Formal verification of logic controller specification rusing NuSMV model checker, X Międzynarodowe Warsztaty Doktoranckie OWD’2008, Archiwum konferencji PTETIS, Vol. 25, pp. 459-464.
• [15] Huth M., Ryan M., 2004. Logic in Computer Science. Modelling and Reasoning about Systems, Cambridge University Press.
• [16] Kern C., Greenstreet M.R., 1999. Formal Verification in Hardware Design: A Survey, ACM Transactions on Design Automation of Electronic Systems (TODAES), Vol. 4, Issue 2, pp. 123-193.
• [17] Klimek R., 1999. Wprowadzenie do logiki temporalnej, AGH Uczelniane Wydawnictwa Naukowo-Dydaktyczne, Kraków (in Polish).
• [18] Lamport L., 1980. “Sometime” is sometimes “not never”, On the Temporal Logic of Programs, Proceedings of the Seventh ACM Symposium on Principles of Programming Languages, ACM SIGACT-SIGPLAN, pp. 174-185.
• [19] http://www.omg.org
• [20] 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).
• [21] Staines T.S., 2008. 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, pp. 191-200.
• [22] Tričković I., 2000. Formalizing activity diagram of UML by Petri nets, Novi Sad J. Math, Vol. 30, No. 3, pp. 161-171.
• [23] Yen-Liang C., Sammy C., Chyun-Chyi C., Irene C., 2000. Workflow Process Definition and Their Applications in e-Commerce, IEEE 2000, pp. 193-200.