Regułowa reprezentacja interpretowanych sieci Petriego sterowania dla potrzeb syntezy i weryfikacji

• Autorzy: Grobelna I.

Warianty tytułu

EN

Rule-based representation of Control Interpreted Petri Nets for synthesis and verification purposes

• Języki publikacji: PL

Abstrakty

PL

Artykuł proponuje regułowy sposób reprezentacji interpretowanych sieci Petriego sterowania w logice temporalnej. Sposób ten jest przydatny zarówno do formalnej weryfikacji modelowej, jak i do automatycznej syntezy logicznej z wykorzystaniem języków opisu sprzętu (Verilog, VHDL) jako rekonfigurowalny sterownik logiczny lub PLC. Sieci Petriego weryfikowane są zwykle tylko pod kątem właściwości strukturalnych. Technika weryfikacji modelowej pozwala na weryfikację właściwości behawioralnych opisujących zachowanie projektowanego systemu.

EN

The paper presents a novel idea of Control Interpreted Petri Nets representation in temporal logic. The proposed logic representation is suitable both for formal model checking and automatic synthesis using hardware description languages (Verilog, VHDL). Petri Nets [1, 2, 3] are currently used in industry, i.e. by logic controller design [4]. Dedicated tools for creating Petri Nets support verification against structural properties. Behavioral properties are also of great importance, however they are rarely considered. Model checking technique [5] allows for verification of properties describing behavior of designed system. So far, there have been some approaches to verify (validate) specification by means of Petri Nets [6, 7, 8, 9], by means of UML diagrams [10] or logic controller programs in ST language [11]. However, none of them have addressed Control Interpreted Petri Nets focused on RTL level. The proposed rule-based representation of Control Interpreted Petri Nets (logical model in Figs. 2-5) is easy to formally verify (model description for NuSMV model checker [13] in Fig. 6-10), as well as to synthezise (VHDL model in Figs. 11-13) as a reconfigurable logic controller or PLC. Verified behavioral specification in temporal logic [14] is an abstract program of matrix reconfigurable logic controller functionality, and logic controller program (implementation) satisfies its primary specification. The logical model built from Control Inter-preted Petri Net describes it in a strict and short form.

Słowa kluczowe

PL

weryfikacja modelowa; interpretowane sieci Petriego sterowania; synteza logiczna

EN

model checking; control interpreted Petri nets

• Wydawca: Wydawnictwo PAK
• Czasopismo: Pomiary Automatyka Kontrola
• Rocznik: 2011
• Tom: R. 57, nr 8
• Strony: 942--944
• Opis fizyczny: Bibliogr. 15 poz., rys., wzory

Twórcy

autor

Grobelna I.

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

Bibliografia

• [1] Adamski M.: A rigorous design methodology for reprogrammable logic controllers, The International Workshop on Discrete-Event System Design, DESDes’01, June 2001, Przytok.
• [2] David R., Alla H.: Petri Nets & Grafcet. Tools for modelling discrete event systems, Prentice Hall 1992.
• [3] Adamski M., Karatkevich A., Węgrzyn M. (ed.): Design of embedded control systems, Springer 2005.
• [4] Gomes L., Barros J. P., Costa A.: Modeling formalisms for embedded system design, Embedded Systems Handbook, Taylor & Francis Group, LLC, 2006.
• [5] 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.
• [6] Berthomieu B., Peres F., Vernadat F.: Model checking bounded prioritized time Petri nets, ATVA’07 Proceedings of the 5th international conference on Automated technology for verification and analysis, 2007.
• [7] Cortés L. A., Eles P., Peng Z.: Formal coverification of embedded systems using model checking, Proceesings of the 26th EUROMICRO Conference (EUROMICRO’00), 2000 IEEE.
• [8] Penczek W., Półrola A.: Advances in verification of Time Petri Nets and timed automata, Springer 2006.
• [9] Ribeiro Ó. R., Fernades J. M.: Translating synchronous Petri Nets into PROMELA for verifying behavioural properties, IEEE 2007.
• [10] Niewiadomski A., Penczek W., Szreter M.: Towards checking parametric reachability for UML state machines, Novosibirsk University 2009, Proc of. 7th International Andrei Ershov Memorial Conference Perspectives of System Informatics, str. 229-240.
• [11] Gourcuff V., De Smet O., Faure J. M.: Efficient representation for formal verification of PLC programs, Discrete Event Systems, 2006, 8th International Workshop, pp. 182-187.
• [12] 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, str. 607-612.
• [13] Cavada R. et al.: NuSMV 2.5 user manual, dostępne na http:// nusmv.fbk.eu/
• [14] Ben-Ari M.: Logika matematyczna w informatyce. Klasyka informatyki. Wydawnictwa Naukowo-Techniczne, Warszawa 2005.
• [15] Węgrzyn M.: Modelowanie sieci Petriego w języku VHDL, Przegląd Elektrotechniczny, 2010, nr 1, str. 212-216.