Geodesic
Using X-CTL logic to implement  formal verification of X-machines
Informacionnye tehnologii i vyčislitelnye sistemy, no. 3 (2010), pp. 47-52

Voir la notice de l'article provenant de la source Math-Net.Ru

The article contains the review of CTL logic and its application to formal verification. X-CTL logic is proposed, allowing implementing the formal verification of X-machines. The sample model of a counter is presented.
Keywords: Formal verification, model checking, X-Machine, complex systems. 
@article{ITVS_2010_3_a5,
     author = {M. S. Sobolev},
     title = {Using {X-CTL} logic to implement~ formal verification of {X-machines}},
     journal = {Informacionnye tehnologii i vy\v{c}islitelnye sistemy},
     pages = {47--52},
     publisher = {mathdoc},
     number = {3},
     year = {2010},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/ITVS_2010_3_a5/}
}
TY  - JOUR
AU  - M. S. Sobolev
TI  - Using X-CTL logic to implement  formal verification of X-machines
JO  - Informacionnye tehnologii i vyčislitelnye sistemy
PY  - 2010
SP  - 47
EP  - 52
IS  - 3
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/ITVS_2010_3_a5/
LA  - ru
ID  - ITVS_2010_3_a5
ER  - 
%0 Journal Article
%A M. S. Sobolev
%T Using X-CTL logic to implement  formal verification of X-machines
%J Informacionnye tehnologii i vyčislitelnye sistemy
%D 2010
%P 47-52
%N 3
%I mathdoc
%U http://geodesic.mathdoc.fr/item/ITVS_2010_3_a5/
%G ru
%F ITVS_2010_3_a5
M. S. Sobolev. Using X-CTL logic to implement  formal verification of X-machines. Informacionnye tehnologii i vyčislitelnye sistemy, no. 3 (2010), pp. 47-52. http://geodesic.mathdoc.fr/item/ITVS_2010_3_a5/