Geodesic
LTL Verification of Automaton Programs
Modelirovanie i analiz informacionnyh sistem, Tome 14 (2007) no. 1, pp. 31-43 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice de l'article

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. 
@article{MAIS_2007_14_1_a4,
     author = {K. A. Vasileva and E. V. Kuzmin},
     title = {LTL {Verification} of {Automaton} {Programs}},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {31--43},
     year = {2007},
     volume = {14},
     number = {1},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2007_14_1_a4/}
}
TY  - JOUR
AU  - K. A. Vasileva
AU  - E. V. Kuzmin
TI  - LTL Verification of Automaton Programs
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2007
SP  - 31
EP  - 43
VL  - 14
IS  - 1
UR  - http://geodesic.mathdoc.fr/item/MAIS_2007_14_1_a4/
LA  - ru
ID  - MAIS_2007_14_1_a4
ER  - 
%0 Journal Article
%A K. A. Vasileva
%A E. V. Kuzmin
%T LTL Verification of Automaton Programs
%J Modelirovanie i analiz informacionnyh sistem
%D 2007
%P 31-43
%V 14
%N 1
%U http://geodesic.mathdoc.fr/item/MAIS_2007_14_1_a4/
%G ru
%F MAIS_2007_14_1_a4
K. A. Vasileva; E. V. Kuzmin. LTL Verification of Automaton Programs. Modelirovanie i analiz informacionnyh sistem, Tome 14 (2007) no. 1, pp. 31-43. http://geodesic.mathdoc.fr/item/MAIS_2007_14_1_a4/

[1] A. A. Shalyto, Switch-tekhnologiya. Algoritmizatsiya i programmirovanie zadach logicheskogo upravleniya, Nauka, SPb., 1998, 628 pp. http://is.ifmo.ru/books/switch/1/ | Zbl

[2] A. A. Shalyto, “Avtomatnoe proektirovanie programm. Algoritmizatsiya i programmirovanie zadach logicheskogo upravleniya”, Izvestiya Akademii nauk. Teoriya i sistemy upravleniya, 2000, no. 6, 63–81 http://is.ifmo.ru

[3] A. A. Shalyto, “Algoritmizatsiya i programmirovanie dlya zadach logicheskogo upravleniya i «reaktivnykh» sistem”, Avtomatika i telemekhanika. Obzory, 2001, no. 1, 3–39 http://is.ifmo.ru | Zbl

[4] A. A. Shalyto, N. I. Tukkel, “SWITCH-tekhnologiya avtomatnyi podkhod k sozdaniyu programmnogo obespecheniya «reaktivnykh» sistem”, Programmirovanie, 2001, no. 5, 45–62 http://is.ifmo.ru/works/switch/1/ | Zbl

[5] E. V. Kuzmin, “Ierarkhicheskaya model avtomatnykh programm”, Modelirovanie i analiz informatsionnykh sistem, 13:1 (2006), 27–34

[6] E. M. Klark, O. Gramberg, D. Peled, Verifikatsiya modelei programm: Model Checking, MTsNMO, 2002, 416 pp.

[7] E. V. Kuzmin, V. A. Sokolov, Strukturirovannye sistemy perekhodov, FIZMATLIT, M., 2006, 178 pp. | MR

[8] E. V. Pervushin, A. A. Shalyto, Modelirovanie bankomata, SPbGU ITMO, 2003 http://is.ifmo.ru/projects/

[9] SPIN, http://spinroot.com/spin/whatispin.html