Automatyczna weryfikacja i synteza regułowego modelu sterownika logicznego

• Autorzy: Grobelna I.
• Języki publikacji: PL

Abstrakty

EN

The article focuses on model checking and synthesis of rule-based specification of logic controller. It describes and illustrates proposed design system of logic controllers. Specification by means of Control Interpreted Petri Nets is formally written as rule-based logical model, which is suitable both for formal verification against behavioral requirements and for synthesis in form of reconfigurable logic controller. Verifiable model is thereby consistent with synthesizable model. Logical model is also used for behavioral verification and simulation. Translation process of rule-based specification into verifiable model description and synthesizable code has been automated.

Słowa kluczowe

PL

sterownik logiczny; specyfikacja; sprawdzanie modelu; synteza

EN

logic controller; specification; model checking; synthesis

• Wydawca: Komisja Informatyki Polskiej Akademii Nauk, Oddział w Gdańsku
• Czasopismo: Metody Informatyki Stosowanej
• Rocznik: 2011
• Tom: nr 3
• Strony: 59--65
• Opis fizyczny: Bibliogr. 22 poz., rys.

Twórcy

autor

Grobelna I.

• Uniwersytet Zielonogórski, Wydział Elektrotechniki, Informatyki i Telekomunikacji

Bibliografia

• [1] Adamski M. A rigorous design methodology for reprogrammable logic controllers. The International Workshop on Discrete-Event System Design, DESDes’01, 2001
• [2] Adamski M., Chodań M. Modelowanie układów sterowania dyskretnego z wykorzystaniem sieci SFC, Wydawnictwo Politechniki Zielonogórskiej, 2000
• [3] Ben-Ari M. Logika matematyczna w informatyce. Klasyka informatyki. Wydawnictwa Naukowo-Techniczne, Warszawa 2005
• [4] Cavada R. et al. NuSMV 2.5 User Manual. Pobrane ze strony http://nusmv.fbk.eu/ (dostęp: 31.10.2011)
• [5] Clarke E.M., Grumberg O., Peled D.A. Model checking. The MIT Press, 1999
• [6] David R., Alla H., Discrete, Continuous, and Hybrid Petri Nets, Springer-Verlag Berlin Heidelberg 2010
• [7] Gomes L., Barros J. P., Costa A. Modeling Formalisms for Embedded System Design,Embedded Systems Handbook, Taylor & Francis Group, LLC, 2006
• [8] Grobelna I. Weryfikacja modelowa z NuSMV. Oficyna Wydawnicza Uniwersytetu Zielonogórskiego, 2011
• [9] Grobelna I. Weryfikacja modelowa interpretowanych sieci Petriego sterowania. Pomiary Automatyka Kontrola, 2011, Vol. 57, nr 6, s. 666-670
• [10] Grobelna I. Regułowa reprezentacja interpretowanych sieci Petriego sterowania dla potrzeb syntezy i weryfikacji. Pomiary Automatyka Kontrola, 2011, Vol. 57, nr 8, s. 942-944
• [11] Grobelna I. Formalna analiza interpretowanych algorytmicznych maszyn stanów ASM z wykorzystaniem narzędzia model checker, Metody Informatyki Stosowanej nr 3/2008, Tom 16, s. 107-124
• [12] Grobelna I., Grobelny M. Gaps in design and tests of dependable embedded systems, Metody Informatyki Stosowanej, 2010, nr 2, s. 45-51 Automatyczna weryfikacja i synteza regułowego modelu sterownika logicznego 65
• [13] Grobelna I. Formal verification of embedded logic controller specification with computer deduction in temporal logic. Przegląd Elektrotechniczny, r. 87 nr 12/2011, s. 47-50
• [14] 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, Polska, 2011, s. 621-626 (dostępne w IEEE Xplore)
• [15] 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. Wrocław, Polska, 2010, s. 607-612 (dostępne w IEEE Xplore)
• [16] De Micheli G., Synteza i optymalizacja układów cyfrowych, Wydawnictwa Naukowo-Techniczne WNT 1998
• [17] Pardey J., Bolton M. Logic synthesis of synchronous parallel controllers. Computer Design: VLSI in Computers and Processors, 1991, ICCD’91. Proceedings, s. 454-457
• [18] Pawłowski M., Skorupski A. Projektowanie złożonych układów cyfrowych. Wydawnictwa Komunikacji i Łączności, 2010
• [19] Węgrzyn M., Węgrzyn A. PeNLogic – System for Concurrent Logic Controllers Design, W: Adamski M., Barkalov A., Węgrzyn M. (Eds.), Design of Digital Systems and Devices, Lecture Notes in Electrical Engineering, Vol. 79, Springer Verlag, 2011, s. 215-228
• [20] WoPeD homepage: www.woped.org
• [21] Zieliński C. Podstawy projektowania układów cyfrowych, Wydawnictwo Naukowe PWN, Warszawa 2003
• [22] Zwoliński M. Projektowanie układów cyfrowych z wykorzystaniem języka VHDL. Wydawnictwa Komunikacji i Łączności, 2007