Verification of declarative LTL-specification of control programs behavior
| Autor: | Maxim V. Neyzov, Egor V. Kuzmin |
|---|---|
| Jazyk: | English<br />Russian |
| Rok vydání: | 2024 |
| Předmět: | |
| Zdroj: | Моделирование и анализ информационных систем, Vol 31, Iss 2, Pp 120-141 (2024) |
| Druh dokumentu: | article |
| ISSN: | 1818-1015 2313-5417 |
| DOI: | 10.18255/1818-1015-2024-2-120-141 |
| Popis: | The article continues the series of works on development and verification of control programs based on LTL-specifications of a special type. Previously, it was proposed a declarative LTL-specification, which allows describing the behavior of control programs and building program code based on it in the imperative ST-language for programmable logic controllers. The LTL-specification can be directly verified for compliance with specified temporal properties by the model checking method using the nuXmv symbolic verification tool. In general, it is not required translating LTL-formulas of the specification into another formalism — an SMV-specification (code in the input language of the nuXmv tool). The purpose of this work is to explore alternative ways of representing a program behavior model corresponding to the declarative LTL-specification during its verification within the nuXmv tool. In the article, we transform the declarative LTL-specification into various SMV-specifications with accompanying changes of formulation of the verification problem, what leads to a significant reduction in time costs when checking temporal properties by using the nuXmv tool. The acceleration of verification is due to the reduction of the state space of a model being verified. The SMV-specifications obtained as a result of the proposed transformations specify identical or bisimulationally equivalent transition systems. It is ensuring the same verification results when replacing one SMV-specification with another. |
| Databáze: | Directory of Open Access Journals |
| Externí odkaz: |
|