- Tytuł:
-
Formalna weryfikacja maszyny stanów z wykorzystaniem logiki temporalnej
Formal verification of a state machine with use of temporal logic - Autorzy:
- Grobelna, I.
- Powiązania:
- https://bibliotekanauki.pl/articles/154298.pdf
- Data publikacji:
- 2009
- Wydawca:
- Stowarzyszenie Inżynierów i Techników Mechaników Polskich
- Tematy:
-
algorytmiczne maszyny stanów ASM
logika temporalna
technika Model Checking
algorithmic state machines ASM
temporal logic
formal verification of specification
Model Checking technique - Opis:
-
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.
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). - Źródło:
-
Pomiary Automatyka Kontrola; 2009, R. 55, nr 7, 7; 457-460
0032-4140 - Pojawia się w:
- Pomiary Automatyka Kontrola
- Dostawca treści:
- Biblioteka Nauki
Artykuł