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/

[1] D. Gris, Nauka programmirovaniya, Per. s angl., Mir, M., 1984, 416 pp.

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

[3] E. Parr, Programmiruemye kontrollery: rukovodstvo dlya inzhenera, BINOM. Laboratoriya znanii, M., 2007, 516 pp.

[4] E. V. Kuzmin, V. A. Sokolov, “O verifikatsii LD-programm logicheskikh kontrollerov”, Modelirovanie i analiz informatsionnykh sistem, 19:2 (2012), 138–144 | MR

[5] I. V. Petrov, Programmiruemye kontrollery. Standartnye yazyki i priemy prikladnogo proektirovaniya, SOLON-Press, M., 2004, 256 pp.

[6] CoDeSys. Controller Development System http://www.3s-software.com/

[7] SMV. The Cadence SMV Model Checker http://www.kenmcmil.com/smv.html