Inhibitor and enabling arcs in logic controller design

• Autorzy: Grobelna I. , Grobelny M.

Warianty tytułu

PL

Łuki zakazujące i zezwalające w projektowaniu sterowników logicznych

• Języki publikacji: EN

Abstrakty

EN

The paper presents a novel approach to rule-based logic controller specification and its verification. The proposed abstract model is suited for formal verification (using model checking technique) as well as for logic synthesis (using hardware description language VHDL). Special focus is put on Interpreted Petri Nets with inhibitor and enabling arcs, their realization in rule-based model and, additionally, their interpretation in another logic controller specification technique - UML Activity Diagrams (version 2.x).

PL

Artykuł przedstawia nowatorskie podejście do regułowej specyfikacji sterownika logicznego, wraz z jej weryfikacją (walidacją). Proponowany abstrakcyjny model logiczny jest dogodny zarówno do formalnej weryfikacji modelowej, jak również do syntezy logicznej (język opisu sprzętu VHDL). Szczególną uwagę poświęcono łukom zakazującym i zezwalającym interpretowanych sieci Petriego. Po krótkim wprowadzeniu do omawianej tematyki (rozdział 2), przedstawiono przykład interpretowanej sieci Petriego z łukami zakazującymi i zezwalającymi (rys. 1). Podano sposób ich realizacji w abstrakcyjnym modelu logicznym (rozdział 3, schemat kompletnego proponowanego systemu na rys. 2 oraz przykład regułowego modelu sterownika logicznego na rys. 3). Zaproponowano interpretację łuków zakazujących i zezwalających sieci Petriego w innej postaci specyfikacji zachowania sterownika logicznego (rozdział 4) - diagramach aktywności języka UML (w wersji 2.x). Ze względu na bezstanowość diagramów aktywności, nie jest możliwe bezpośrednie odwzorowanie rozpatrywanych łuków. W artykule zaproponowano dwa rozwiązania - opierające się na wprowadzeniu dodatkowego sygnału (rys. 4a) oraz alternatywne - bazujące na etykietowaniu przepływów (rys. 4b). Przedstawiono sposób formalnej weryfikacji tak przygotowanej specyfikacji regułowej oraz jej syntezy logicznej (rozdział 5). Publikacja kończy się podsumowaniem oraz wnioskami (rozdział 6)

Słowa kluczowe

EN

logic controller specification; formal verification; Petri nets inhibitor and enabling arcs; UML activity diagrams

PL

specyfikacja sterownika logicznego; formalna weryfikacja; łuki zakazujące i zezwalające sieci Petriego; diagramy aktywności języka UML

• Wydawca: Wydawnictwo PAK
• Czasopismo: Pomiary Automatyka Kontrola
• Rocznik: 2012
• Tom: R. 58, nr 6
• Strony: 510--513
• Opis fizyczny: Bibliogr. 15 poz., rys., schem.

Twórcy

autor

Grobelna I.

autor

Grobelny M.

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

Bibliografia

• [1] Adamski M., Karatkevich A., Wegrzyn M. (ed.): Design of embedded control systems. Springer 2005 (USA).
• [2] Kropf T.: Introduction to Formal Hardware Verification. Berlin Heidelberg: Springer-Verlag, 1999.
• [3] Gomes L., Barros J. P., Costa A.: Modeling formalisms for embedded system design. Embedded Systems Handbook, Taylor & Francis Group, 2006.
• [4] David R., Alla H.: Discrete, Continuous, and Hybrid Petri Nets. Berlin Heidelberg: Springer-Verlag, 2010.
• [5] Girault C., Valk R.: Petri Nets for Systems Engineering, A Guide to Modelling, Verification and Applications. Berlin Heidelberg: Springer-Verlag, 2003.
• [6] Unified Modelling Language homepage: www.uml.org
• [7] Clarke E. M., Grumberg O., Peled D. A.: Model checking. Cambridge, The MIT Press, 1999.
• [8] Ribeiro Ó. R., Fernades J. M.: Translating synchronous Petri Nets into PROMELA for verifying behavioural properties. International Symposium on Industrial Embedded Systems, 2007, pp. 266-273.
• [9] 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 : proceedings of the 17th international conference, 2010, pp. 607-612.
• [10] Eshuis R.: Semantics and Verification of UML Activity Diagrams for Workflow Modelling (PhD thesis), University of Twente, Wierden, 2002.
• [11] Grobelna I., Adamski M.: Model checking of control interpreted Petri nets. Mixed Design of Integrated Circuits and Systems - MIXDES 2011 : proceedings of the 18th international conference, 2011, pp. 621-626.
• [12] Grobelna I.: Formal verification of embedded logic controller specification with computer deduction in temporal logic. Electrical Review, 2011, nr 12a, pp. 47-50.
• [13] Karatkevich A., Andrzejewski G.: Analiza wybranych własności interpretowanej sieci Petriego metodą optymalnej symulacji, Pierwsza Krajowa Konferencja Elektroniki - KKE 2002, Polska, 2002, T. 2, pp. 685-690 (in Polish).
• [14] Ben-Ari M.: Mathematical Logic for Computer Science. Berlin Heidelberg: Springer-Verlag, 2001.
• [15] Pardey J., Bolton M.: Logic synthesis of synchronous parallel controllers. Proc. International Conference on Computer Design: VLSI in Computer & Processors, Cambridge, 1991, pp. 454-457.