Formalna weryfikacja maszyny stanów z wykorzystaniem logiki temporalnej

• Autorzy: Grobelna I.

Warianty tytułu

EN

Formal verification of a state machine with use of temporal logic

• Języki publikacji: PL

Abstrakty

PL

Artykuł przedstawia koncepcję specyfikacji współbieżnego procesu sterowania cyfrowego za pośrednictwem diagramów algorytmicznych maszyn stanów ASM w języku aprobowanym przez profesjonalne narzędzie model checker. Specyfikacja może zostać następnie formalnie zweryfikowana pod kątem wymagań stawianych projektowanemu systemowi. Lista wymagań tworzona jest przy wykorzystaniu liniowej logiki temporalnej LTL. Formalna weryfikacja Model Checking polega na sprawdzeniu, czy model systemu spełnia stawiane mu wymagania. W przypadku wykrycia niespóności generowany jest odpowiedni kontrprzykład.

EN

The paper presents the formal specification method of concurrent control processes in form of algorithmic state machines ASM [5] in a language accepted by a professional model checker tool NuSMV. Basing on linear temporal logic LTL [7, 8, 9, 16] a requirement list (Fig. 6) for the system model is prepared. Formal verification Model Checking [17, 19] consists in comparison of the model description and the requirements list. If some requirements cannot be fulfilled, the appropriate counterexample is generated (Fig. 7), which allows localizing the error source. The ASM diagrams (Fig. 4) are fully determined, but they do not support modularity, that is why they are not well suited for specification of concurrent controlling processes. The paper includes a short introduction to the theory of algorithmic state machines ASM (Section 2), temporal logic (Section 3) and model checking technique (Section 4). The proposed solution is presented on an example (Section 5) of the process of controlling (partially concurrent) movements of two vehicles (Fig. 2). The formal verification method of the ASM diagrams with its advantages and disadvantages as well as the general conclusions are given at the end of the paper (Section 6).

Słowa kluczowe

PL

algorytmiczna maszyna stanów; ASM; logika temporalna; technika Model Checking

EN

algorithmic state machines ASM; temporal logic; formal verification of specification; Model Checking technique

• Wydawca: Wydawnictwo PAK
• Czasopismo: Pomiary Automatyka Kontrola
• Rocznik: 2009
• Tom: R. 55, nr 7
• Strony: 457--460
• Opis fizyczny: Bibliogr. 19 poz., rys., tab., wzory

Twórcy

autor

Grobelna I.

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

Bibliografia

• [1] C. Kern, M. R. Greenstreet: Formal Verification in Hardware Design: A Survey. ACM Transactions on Design Automation of Electronic Systems (TODAES), Vol. 4, Issue 2, kwiecień 1999, str. 123–193.
• [2] E. M. Clarke, J. M. Wing et al.: Formal methods: State of the Art and Future Directions. ACM Computing Surveys, Vol. 28, No. 4, grudzień 1996.
• [3] G. Andrzejewski: Programowy model interpretowanej sieci Petriego dla potrzeb projektowania mikrosystemów cyfrowych. Oficyna Wydawnicza Uniwersytetu Zielonogórskiego 2003, str. 16–26.
• [4] L. Gomes, J. P. Barros, A. Costa: Modeling Formalisms for Embedded System Design. Embedded Systems Handbook, Taylor & Francis Group, LLC, 2006.
• [5] J. P. Davis, H. A. Wake, C. Leehaug, J. Branton, N. Namilae: Design versus Programming in Custom Computing Machine Applications: Experiences Using the Algorithmic State Machine Method. Proceedings Military Applications of Programmable Logic Devices – MAPLD-2004, Washington, DC, 8-10 września 2004.
• [6] M. G. Arnold, J. R. Cowles, R. D. Joslin, J. J. Cupal: Simulation of cooperating algorithmic state machines using Verilog HDL. International Conference on Simulation and Hardware Description Languages (ICSHDL), 24-26 stycznia 1994, Tempe, Arizona, (edytorzy P. A. Widsey oraz D. Rhodes), The Society for Computer Simulation, str. 63–69.
• [7] R. Klimek: Wprowadzenie do logiki temporalnej. AGH Uczelniane Wydawnictwa Naukowo-Dydaktyczne, Kraków 1999.
• [8] M. Huth, M. Ryan: Logic in Computer Science. Modelling and Reasoning about Systems. Cambridge University Press 2004.
• [9] M. Ben-Ari: Logika matematyczna w informatyce. Klasyka informatyki. Wydawnictwa Naukowo-Techniczne, Warszawa 2005.
• [10] R. Eshuis: Symbolic Model Checking of UML Activity Diagrams. ACM Transactions on Software Engineering and Methodology, Vol. 15, No 1, styczeń 2006, str. 1–38.
• [11] R. Cavada et al.: NuSMV 2.4 User Manual.
• [12] K. L. McMillan, The SMV system for SMV version 2.5.4.
• [13] An introduction to model checking, By Girish Keshav Palshikar, Courtesy of Embedded Systems Programming, February 2004, www.embedded.com.
• [14] I. Grobelna: Formal verification of logic controller specification using NuSMV model checker. X Międzynarodowe Warsztaty Doktoranckie OWD’2008, Archiwum konferencji PTETIS, Vol. 25, październik 2008, str. 459–464.
• [15] M. Adamski, M. Chodań: Modelowanie układów sterowania dyskretnego z wykorzystaniem sieci SFC. Wydawnictwo Politechniki Zielonogórskiej, Zielona Góra 2000.
• [16] L. Lamport: “Sometime” is sometimes “not never”, On the Temporal Logic of Programs, Proceedings of te Seventh ACM Symposium on Principles of Programming Languages, ACM SIGACT-SIGPLAN 1980, str. 174–185.
• [17] E. M. Clarke, E. A. Emerson, A. P. Sistla: 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.
• [18] I. Grobelna: Formalna analiza interpretowanych algorytmicznych maszyn stanów ASM z wykorzystaniem narzędzia model checker, Metody Informatyki Stosowanej. Przyjęte do publikacji.
• [19] E. A. Emerson: 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.