Geodesic
On Construction and Verification of PLC-Programs
Modelirovanie i analiz informacionnyh sistem, Tome 19 (2012) no. 4, pp. 25-36

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

We review some methods and approaches to programming discrete problems for Programmable Logic Controllers on the example of constructing PLC-programs for controling a code lock. For these approaches we evaluate the usability of the model checking method for the analysis of program correctness with respect to the automatic verification tool Cadence SMV. Some possible PLC-program vulnerabilities arising at a number approaches to programming of PLC are revealed.
Keywords: PLC-programs, verification, model checking. 
@article{MAIS_2012_19_4_a1,
     author = {E. V. Kuzmin and V. A. Sokolov},
     title = {On {Construction} and {Verification} of {PLC-Programs}},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {25--36},
     publisher = {mathdoc},
     volume = {19},
     number = {4},
     year = {2012},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2012_19_4_a1/}
}
TY  - JOUR
AU  - E. V. Kuzmin
AU  - V. A. Sokolov
TI  - On Construction and Verification of PLC-Programs
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2012
SP  - 25
EP  - 36
VL  - 19
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2012_19_4_a1/
LA  - ru
ID  - MAIS_2012_19_4_a1
ER  - 
%0 Journal Article
%A E. V. Kuzmin
%A V. A. Sokolov
%T On Construction and Verification of PLC-Programs
%J Modelirovanie i analiz informacionnyh sistem
%D 2012
%P 25-36
%V 19
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2012_19_4_a1/
%G ru
%F MAIS_2012_19_4_a1
E. V. Kuzmin; V. A. Sokolov. On Construction and Verification of PLC-Programs. Modelirovanie i analiz informacionnyh sistem, Tome 19 (2012) no. 4, pp. 25-36. http://geodesic.mathdoc.fr/item/MAIS_2012_19_4_a1/