Formal verification of embedded logic controller specification with computer deduction in temporal logic

• Autorzy: Grobelna I.

Warianty tytułu

PL

Formalna weryfikacja specyfikacji wbudowanych sterowników logicznych z wykorzystaniem wnioskowania komputerowego w logice temporalnej

• Języki publikacji: EN

Abstrakty

EN

The article presents a novel approach to formal verification of logic controller specification. Model checking technique is used to verify some behavioral properties. The approach proposes to use a rule-based logical model presented at RTL-level. Proposed logical model is suitable both for formal verification (model checking in the NuSMV tool) and for logical synthesis (using hardware description language VHDL). As the result, logic controller program (its implementation) will be valid according to its primary specification.

PL

Artykuł przedstawia nowatorskie podejście do formalnej weryfikacji specyfikacji sterownika logicznego. Zaproponowany został regułowy model logiczny, który jest dogodny zarówno do formalnej weryfikacji (weryfikacja modelowa w narzędziu NuSMV), jak również do syntezy logicznej (z użyciem języku opisu sprzętu VHDL). Program sterownika logicznego (jego implementacja) będzie zatem poprawny względem początkowej specyfikacji.

Słowa kluczowe

EN

formal verification; embedded logic controllers; temporal logic; electrical technology; electrical power engineering

PL

formalna weryfikacja; wbudowane sterowniki logiczne; logika temporalna; elektrotechnika; elektroenergetyka

• Wydawca: Wydawnictwo SIGMA-NOT
• Czasopismo: Przegląd Elektrotechniczny
• Rocznik: 2011
• Tom: R. 87, nr 12a
• Strony: 47--50
• Opis fizyczny: Bibliogr. 29 poz., il., tabl., wykr.

Twórcy

autor

Grobelna I.

• University of Zielona Gora, ul. Podgorna 50, 65-246 Zielona Gora, Poland,

Bibliografia

• [1] Grobelna I., Grobelny M., Gaps in design and tests of dependable embedded systems, Metody Informatyki Stosowanej (2010) nr 2, 45 - 51.
• [2] Adamski M., Karatkevich A., Wegrzyn M. (ed.), Design of embedded control systems, Springer 2005 (USA).
• [3] David R., Alla H., Discrete, Continuous, and Hybrid Petri Nets, Springer-Verlag Berlin Heidelberg (2010).
• [4] Adamski M., A rigorous design methodology for reprogrammable logic controllers, The International Workshop on Discrete-Event System Design, DESDes'01 (2001) Poland.
• [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), 27 - 45.
• [6] Clarke E.M., Wing J.M. et al, Formal methods: state of the art and future directions, ACM Computing Surveys Vol. 28, (1996), No. 4.
• [7] Kern C., Greenstreet M.R., Formal verification in hardware design: a survey, ACM Transactions on Design Automation of Electronic Systems (TODAES), Vol. 4, (1999), Issue 2, 123 - 193.
• [8] Fix L., Fifteen years of formal property verification in Intel, Lecture Notes in Computer Science (LNCS), Vol. 5000/2008, O. Grumberg, H. Veith (Eds.), (2008), 139 - 144.
• [9] Niewiadomski A., Penczek W., Szreter M., Towards checking parametric reachability for UML state machines, Proc of. 7th International Andrei Ershov Memorial Conference Perspectives of System Informatics, (2009), 229 - 240.
• [10] Lam V.S.W., Padget J., Symbolic Model Checking of UML Statechart Diagrams with an Integrated Approach, Proceedings of the 11th IEEE International Conference and Wrokshop on the Engineering of Computer-Based Systems (ECBS’04), (2004).
• [11] Broel-Plater B., Uklady wykorzystujace sterowniki PLC. Projektowanie algorytmów sterowania, Wydawnictwo Naukowe PWN SA (2008).
• [12] Gourcuff V., De Smet O., Faure J.-M., Efficient representation for formal verification of PLC programs, Discrete Event Systems, 8th International Workshop, (2006), 182 - 187.
• [13] Lampériere-Couffin S., Lesage J.J., Formal Verification of the Sequential Part of PLC Programs, 5th Workshop on Discrete Event Systems (WODES 2000), Ghent, (2000), 247 - 254.
• [14] Bauer N., Engell S., Huuck R., Lohmann S., Lukoschus B., Remelhe M., Stursberg O., Verification of PLC Programs given as Sequential Function Charts, Proceedings of SoftSpez Final Report, (2004), 517 - 540.
• [15] Penczek W., Półrola A., Advances in verification of Time Petri Nets and timed automata, Springer (2006).
• [16] 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).
• [17] Cortés L.A., Eles P., Peng Z., Formal coverification of embedded systems using model checking, Proceedings of the 26th EUROMICRO Conference (EUROMICRO’00), IEEE (2000).
• [18] Ribeiro O.R., Fernades J.M., Translating synchronous Petri Nets into PROMELA for verifying behavioural properties, IEEE (2007).
• [19] Frey G., Wagner F., A Toolbox for the Development of Logic Controllers using Petri Nets, Proceedings of the 8th International Workshop on Discrete Event Systems (WODES 2006), 473 - 474.
• [20] Cavada R. et al., NuSMV 2.5 user manual, available at http://nusmv.fbk.eu/
• [21] Ben-Ari M., Logika matematyczna w informatyce. Klasyka informatyki. Wydawnictwa Naukowo-Techniczne, Warszawa (2005).
• [22] Huth M., Ryan M., Logic in Computer Science. Modelling and Reasoning about Systems, Cambridge University Press (2004).
• [23] 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), 174 - 185.
• [24] 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 (2001), 1 - 22.
• [25] Kropf T., Introduction to Formal Hardware Verification, Springer-Verlag Berlin Heidelberg New York, (1999).
• [26] WoPeD homepage: www.woped.org.
• [27] PIPE homepage: http://pipe2.sourceforge.net/.
• [28] Węgrzyn M., Modelowanie sieci Petriego w jezyku VHDL, Przeglad Elektrotechniczny, (2010), nr 1, 212 - 216.
• [29] 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, (2010) 607 - 612.