Projektowanie sterowników logicznych z wykorzystaniem łuków zezwalających i zakazujących sieci Petriego

• Autorzy: Grobelna I. , Grobelny M.

Warianty tytułu

EN

Logic controller design using enabling and inhibitor arcs of Petri nets

• Języki publikacji: PL

Abstrakty

PL

Artykuł dotyczy zagadnień związanych z projektowaniem sterowników logicznych z wykorzystaniem łuków zezwalających i zakazujących sieci Petriego. Zaproponowano nowatorskie podejście do regułowej specyfikacji sterownika logicznego, przygotowanej w postaci abstrakcyjnego autorskiego modelu logicznego dogodnego do formalnej weryfikacji modelowej oraz syntezy logicznej. Szczególną uwagę zwrócono tutaj na łuki zakazujące i zezwalające interpretowanych sieci Petriego, ich realizację w abstrakcyjnym modelu logicznym i interpretację w innej postaci specyfikacji zachowania sterownika logicznego - diagramach aktywności języka UML.

EN

The paper focuses on logic controller design using enabling and inhibitor arcs of Petri nets. There is proposed a novel original approach to rule-based specification of logic controller behaviour prepared as an abstract logical model suitable for formal verification and logic synthesis. Special interest is put on enabling and inhibitor (disabling) arcs of interpreted Petri nets, their realization in an abstract logical model and interpretation in other specification form - namely UML activity diagrams (in version 2.x). These arcs can be used for flow synchronization or controlled usage of shared resources. After a short introduction (Section 1), some basic concepts on logic controller specification are presented (Section 2), in particular considering (interpreted) Petri nets and UML (activity) diagrams. Usage of enabling and inhibitor arcs is shown on an example of the interpreted Petri net in Fig. 1 (transitions firing sequence in Fig. 2), followed by their representation in the proposed abstract rule-based logical model, its formal verification (using model checking technique) and synthesis (Section 3). The paper also proposes enabling and inhibitor arcs interpretation in UML activity diagrams (Section 4). Although direct representation of these arcs is not possible, the authors try to achieve an alternative solution which corresponds semantically to appropriate Petri net elements. Tab. 1 presents graphic representation of the considered arcs in interpreted Petri nets as well as in UML activity diagrams. The paper ends with a short summary (Section 5).

Słowa kluczowe

PL

specyfikacja behawioralna; rekonfigurowalny sterownik logiczny; UML; diagramy aktywności

EN

behavioural specification; UML; reconfigurable logic controller; activity diagrams

• Wydawca: Wydawnictwo PAK
• Czasopismo: Pomiary Automatyka Kontrola
• Rocznik: 2012
• Tom: R. 58, nr 7
• Strony: 605--607
• Opis fizyczny: Bibliogr. 11 poz., rys., tab.

Twórcy

autor

Grobelna I.

autor

Grobelny M.

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

Bibliografia

• [1] Gomes L., Barros J. P., Costa A.: Modeling formalisms for embedded system design. Embedded Systems Handbook, Taylor & Francis Group, 2006.
• [2] Girault C., Valk R.: Petri Nets for Systems Engineering, A Guide to Modelling, Verification and Applications. Berlin Heidelberg: Springer-Verlag, 2003.
• [3] David R., Alla H.: Discrete, Continuous, and Hybrid Petri Nets. Berlin Heidelberg: Springer-Verlag, 2010.
• [4] Minns P., Elliott I.: FSM based Digital Design using Verilog HDL. Wiley 2008.
• [5] Strona domowa Unified Modelling Language: www.uml.org
• [6] Łabiak G., Adamski M., Tkacz J., Doligalski M., Bukowiec A.: Role of UML modelling in discrete controller design. ICSEng 2011, Proceedings of 21st International Conference on Systems Engineering, 2011 ss. 480-481.
• [7] 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, ss. 607-612.
• [8] 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, ss. 621-626.
• [9] Grobelna I.: Formal verification of embedded logic controller specification with computer deduction in temporal logic. Electrical Review, 2011, nr 12 a, ss. 47-50.
• [10] Grobelna I.: Regułowa reprezentacja interpretowanych sieci Petriego sterowania dla potrzeb syntezy i weryfikacji. Pomiary Automatyka Kontrola, nr 8, Vol. 57, 2011, ss. 942-944.
• [11] Clarke E. M., Grumberg O., Peled D. A.: Model checking. Cambridge, The MIT Press, 1999.