LTL Verification of Automaton Programs
In the paper one of approaches to modelling, specification and verification of automaton programs are considered. The automata programming technology is effective enough in design and verification (the analysis of correctness) software for reactive and controlling systems. This technology, besides o...
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2007-03-01
|
| Series: | Моделирование и анализ информационных систем |
| Online Access: | https://www.mais-journal.ru/jour/article/view/1112 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849241015242719232 |
|---|---|
| author | K. A. Vasileva E. V. Kuzmin |
| author_facet | K. A. Vasileva E. V. Kuzmin |
| author_sort | K. A. Vasileva |
| collection | DOAJ |
| description | In the paper one of approaches to modelling, specification and verification of automaton programs are considered. The automata programming technology is effective enough in design and verification (the analysis of correctness) software for reactive and controlling systems. This technology, besides other methods of software construction "without errors", is much more constructive, as it allows to begin "struggling against errors" at the algorithmization stage. However, in spite of the fact that the idea of automata programming is directed on the construction of reliable programs, the problem of the program correctness analysis still remains actual. From the point of view of modelling and analysing program systems the automata approach to programming has a number of advantages in comparison with the traditional approach. When constructing a model for a program written in the traditional style, there is a serious problem of the adequacy of this program model to the initial program. The model can be unable to take into account a number of program properties or can generate nonexisting properties. Under the automata programming such a problem is excluded, as a collection of communicating automata, describing the logic of the program, is already an adequate program model. This fact is an indisputable advantage of the automata technology. Moreover, the model has a finite set of states, that is, in practice, a necessary condition for successful automatic verification by the model checking method. Besides, properties of automata programs are naturally and clearly formulated and specified. These properties obviously correspond with communicating automata representing the logic of an automata program. The practical result of the work is an application of the tool SPIN and the temporal logic LTL for specification and verification of hierarchical automaton programs. |
| format | Article |
| id | doaj-art-1fc538e869bf43a78b613e9fe12fea3c |
| institution | Kabale University |
| issn | 1818-1015 2313-5417 |
| language | English |
| publishDate | 2007-03-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj-art-1fc538e869bf43a78b613e9fe12fea3c2025-08-20T04:00:19ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172007-03-011413143853LTL Verification of Automaton ProgramsK. A. Vasileva0E. V. Kuzmin1Ярославский государственный университетЯрославский государственный университетIn the paper one of approaches to modelling, specification and verification of automaton programs are considered. The automata programming technology is effective enough in design and verification (the analysis of correctness) software for reactive and controlling systems. This technology, besides other methods of software construction "without errors", is much more constructive, as it allows to begin "struggling against errors" at the algorithmization stage. However, in spite of the fact that the idea of automata programming is directed on the construction of reliable programs, the problem of the program correctness analysis still remains actual. From the point of view of modelling and analysing program systems the automata approach to programming has a number of advantages in comparison with the traditional approach. When constructing a model for a program written in the traditional style, there is a serious problem of the adequacy of this program model to the initial program. The model can be unable to take into account a number of program properties or can generate nonexisting properties. Under the automata programming such a problem is excluded, as a collection of communicating automata, describing the logic of the program, is already an adequate program model. This fact is an indisputable advantage of the automata technology. Moreover, the model has a finite set of states, that is, in practice, a necessary condition for successful automatic verification by the model checking method. Besides, properties of automata programs are naturally and clearly formulated and specified. These properties obviously correspond with communicating automata representing the logic of an automata program. The practical result of the work is an application of the tool SPIN and the temporal logic LTL for specification and verification of hierarchical automaton programs.https://www.mais-journal.ru/jour/article/view/1112 |
| spellingShingle | K. A. Vasileva E. V. Kuzmin LTL Verification of Automaton Programs Моделирование и анализ информационных систем |
| title | LTL Verification of Automaton Programs |
| title_full | LTL Verification of Automaton Programs |
| title_fullStr | LTL Verification of Automaton Programs |
| title_full_unstemmed | LTL Verification of Automaton Programs |
| title_short | LTL Verification of Automaton Programs |
| title_sort | ltl verification of automaton programs |
| url | https://www.mais-journal.ru/jour/article/view/1112 |
| work_keys_str_mv | AT kavasileva ltlverificationofautomatonprograms AT evkuzmin ltlverificationofautomatonprograms |