Weryfikacja modelowa interpretowanych sieci Petriego sterowania

• Autorzy: Grobelna I.

Warianty tytułu

EN

Model checking of control interpreted Petri Nets

• Języki publikacji: PL

Abstrakty

PL

Artykuł przedstawia oryginalne podejście do weryfikacji modelowej interpretowanych sieci Petriego sterowania. Sieci Petriego są powszechnie wykorzystywane w przemyśle. Najczęściej jednak weryfikowane są pod kątem właściwości strukturalnych, a właściwości behawioralne (mimo ich dużego znaczenia) są pomijane. Technika weryfikacji modelowej pozwala na weryfikację właściwości opisujących zachowanie projektowanego systemu. Model logiczny otrzymany na podstawie istniejącej sieci Petriego sterowania przedstawiany jest na poziomie RTL w taki sposób, że nadaje się zarówno do formalnej weryfikacji, jak i do syntezy logicznej jako rekonfigurowalny sterownik logiczny lub PLC.

EN

The paper introduces a novel approach to model checking with Control Interpreted Petri Nets [15]. Petri Nets [9, 11, 12, 13] are commonly used in the industry. However, they are mostly verified against structural properties, and behavioral properties are out of scope. The model checking technique [3, 7, 8, 21, 22] allows verifying properties which describe behavior of the designed system. Properties to be verified are expressed in temporal logic [16, 17, 18, 19, 20]. The logical model (Fig. 1) derived from existing Petri net is presented at RTL level (Register Transfer Level) in such a way, that it is easy to be formally verified as well as to logical synthesized as a reconfigurable logic controller or PLC (Programmable Logic Controller). It operates on variables which correspond to places, input and output signals of the Control Interpreted Petri Net (Section 3). The variables change their values according to some specified rules. The logical model is afterwards transformed into input format of the NuSMV model checker [23] and formally verified (Section 4). Control Interpreted Petri Net (Fig. 2) is divided into elementary subnets (Fig. 3). Each elementary subnet consists of a single place and its input and output transitions. Each elementary subnet is interpreted as a single segment of model description in the NuSMV tool. Each elementary subnet represents a two-states state machine which is usually realized as a single macrocell (Fig. 4) in the FPGA circuit. The properties to be verified are expressed in LTL or CTL logic. If any of them is not satisfied in the described system model, the appropriate counterexample is generated (Fig. 6). In the example in the paper the verification finds a subtle error resulting from incorrect / incomplete specification (Fig. 5) and allows the user to localize the error source.

Słowa kluczowe

PL

weryfikacja modelowa; sterownik logiczny; interpretowane sieci Petriego sterowania; logika temporalna

EN

model checking; logic controller; control interpreted Petri nets; temporal logic

• Wydawca: Wydawnictwo PAK
• Czasopismo: Pomiary Automatyka Kontrola
• Rocznik: 2011
• Tom: R. 57, nr 6
• Strony: 666--670
• Opis fizyczny: Bibliogr. 30 poz., rys., schem.

Twórcy

autor

Grobelna I.

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

Bibliografia

• [1] Avizienis A., Laprie J., Randell B.: Fundamental concepts of computer system dependability, IARP/IEEE-RAS Workshop on Robot Dependability: Technological Challenge of Dependable Robots in Human Environments, Seoul, Korea, May 2001.
• [2] Khalgui M., Hanisch H. -M.: Reconfiguration of industrial embedded control systems, Tenth International Conference on Application of Concurrency to System Design, ACSD 2010.
• [3] 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.
• [4] Kropf T.: Introduction to Formal Hardware Verification, ISBN 3-540-65445-3, Springer-Verlag Berlin Heidelberg New York, 1999.
• [5] Clarke E. M., Wing J. M. et al.: Formal methods: state of the art and future directions, ACM Computing Surveys, Vol. 28, No. 4, December 1996.
• [6] Kern C., Greenstreet M. R.: Formal Verification in Hardware Design: A Survey, ACM Transactions on Design Automation of Electronic Systems (TODAES), Vol. 4, Issue 2, 1999, str. 123-193.
• [7] Fix L.: Fifteen years of formal property verification in Intel, Lecture Notes in Computer Science (LNCS) 2008, Volume 5000/2008, O. Grumberg, H. Veith (Eds.), str. 139-144, 2008.
• [8] Holzmann G. J., Joshi R., Groce A.: Model driven code checking, Automated Software Engineering, Vol. 15, Issue 3-4, December 2008, str. 283-297.
• [9] Gomes L., Barros J. P., Costa A.: Modeling formalisms for embedded system design, Embedded Systems Handbook, Taylor & Francis Group, LLC, 2006.
• [10] 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.
• [11] Adamski M., Chodań M.: Modelowanie układów sterowania dyskretnego z wykorzystaniem sieci SFC, Wydawnictwo Politechniki Zielonogórskiej 2000.
• [12] Adamski M., Karatkevich A., Węgrzyn M. (ed.): Design of embedded control systems, Springer 2005.
• [13] David R., Alla H.: Petri Nets & Grafcet. Tools for modelling discrete event systems, Prentice Hall 1992.
• [14] Frey G., Litz L: Verification and validation of control algorithms by coupling of Interpreted Petri Nets, Proceedings of the IEEE SMC’98, 1998, Vol. 1, str. 7-12.
• [15] Adamski M.: A rigorous design methodology for reprogrammable logic controllers, The International Workshop on Discrete-Event System Design, DESDes’01, June 2001, Przytok.
• [16] Ben-Ari M.: Logika matematyczna w informatyce. Klasyka informatyki. Wydawnictwa Naukowo-Techniczne, Warszawa 2005.
• [17] Huth M., Ryan M.: Logic in Computer Science. Modelling and Reasoning about Systems, Cambridge University Press 2004.
• [18] Klimek R.: Wprowadzenie do logiki temporalnej, AGH Uczelniane Wydawnictwa Naukowo-Dydaktyczne, Kraków 1999.
• [19] Rice M. V., Vardi M. Y.: Branching vs. Linear Time: Final Showdown, Proceedings of the 2001 Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2001, LNCS Volume 2031, Springer-Verlag, str. 1–22.
• [20] Lamport L.: “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 1980, str. 174-185.
• [21] Clarke E. M., Emerson E. A., Sistla A. P.: Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems, Vol. 8, No. 2, April 1986, str. 244-263.
• [22] Clarke E. M., et al.: Automatic verification of sequential circuit designs, Phil. Trans. R. Soc. Lond. A (1992) 339, str. 105-120.
• [23] Cavada R. et al.:, NuSMV 2.5 user manual, dostępne na http:// nusmv.fbk.eu/
• [24] 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.
• [25] Penczek W., Półrola A.: Advances in verification of Time Petri Nets and timed automata, Springer 2006.
• [26] Cortés L. A., Eles P., Peng Z.: Formal coverification of embedded systems using model checking, Proceedings of the 26th EUROMICRO Conference (EUROMICRO’00), 2000 IEEE.
• [27] Ribeiro Ó. R., Fernades J. M.: Translating synchronous Petri nets into PROMELA for verifying behavioural properties, IEEE 2007.
• [28] Grobelna I.: Formalna analiza interpretowanych algorytmicznych maszyn stanów ASM z wykorzystaniem narzędzia model checker, Metody Informatyki Stosowanej, nr 3/2008 Tom 16, str. 107-124.
• [29] WoPeD homepage: www.woped.org
• [30] PIPE homepage: http://pipe2.sourceforge.net/