Geodesic
Modeling, Specification and Construction of PLC-programs
Modelirovanie i analiz informacionnyh sistem, Tome 20 (2013) no. 2, pp. 104-120.

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

A new approach to construction of reliable discrete PLC-programs with timers — programming based on specification and verification — is proposed. Timers are modelled in a discrete way. For the specification of a program behavior we use the linear-time temporal logic LTL. Programming is carried out in the ST-language according to a LTL-specification. A new approach to programming of PLC is shown by an example. The proposed programming approach provides an ability of a correctness analysis of PLC-programs using the model checking method. The programming requires fulfillment of the following two conditions: 1) a value of each variable should be changed not more than once per one full PLC-program implementation (per one full working cycle of PLC); 2) a value of each variable should only be changed in one place of a PLC-program. Under the proposed approach the change of the value of each program variable is described by a pair of LTL-formulas. The first LTL-formula describes situations that increase the value of the corresponding variable, the second LTL-formula specifies conditions leading to a decrease of the variable value. The LTL-formulas (used for specification of the corresponding variable behavior) are constructive in the sense that they construct the PLC-program, which satisfies temporal properties expressed by these formulas. Thus, the programming of PLC is reduced to the construction of LTL-specification of the behavior of each program variable.
Keywords: programmable pogic controllers, software engineering, modeling and specification of PLC-programs. 
@article{MAIS_2013_20_2_a7,
     author = {E. V. Kuzmin and V. A. Sokolov},
     title = {Modeling, {Specification} and {Construction} of {PLC-programs}},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {104--120},
     publisher = {mathdoc},
     volume = {20},
     number = {2},
     year = {2013},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2013_20_2_a7/}
}
TY  - JOUR
AU  - E. V. Kuzmin
AU  - V. A. Sokolov
TI  - Modeling, Specification and Construction of PLC-programs
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2013
SP  - 104
EP  - 120
VL  - 20
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2013_20_2_a7/
LA  - ru
ID  - MAIS_2013_20_2_a7
ER  - 
%0 Journal Article
%A E. V. Kuzmin
%A V. A. Sokolov
%T Modeling, Specification and Construction of PLC-programs
%J Modelirovanie i analiz informacionnyh sistem
%D 2013
%P 104-120
%V 20
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2013_20_2_a7/
%G ru
%F MAIS_2013_20_2_a7
E. V. Kuzmin; V. A. Sokolov. Modeling, Specification and Construction of PLC-programs. Modelirovanie i analiz informacionnyh sistem, Tome 20 (2013) no. 2, pp. 104-120. http://geodesic.mathdoc.fr/item/MAIS_2013_20_2_a7/

[1] D. Gries, The Science of Programming, Springer-Verlag, 1981 | MR

[2] E. M. Clark, O. Grumberg, D. A. Peled, Model Checking, The MIT Press, 2001

[3] E. V. Kuzmin, V. A. Sokolov, “On Construction and Verification of PLC-Programs”, Modeling and analysis of information systems, 19:4 (2012), 25–36 (in Russian)

[4] E. V. Kuzmin, V. A. Sokolov, “On Verification of PLC-Programs Written in the LD-Language”, Modeling and analysis of information systems, 19:2 (2012), 138–144 (in Russian) | MR

[5] E. A. Parr, Programmable Controllers. An engineer's guide, Newnes, 2003, 442 pp.

[6] I. V. Petrov, Programmiruemye kontrollery. Standartnye jazyki i priemy prikladnogo proektirovanija, SOLON-Press, M., 2004, 256 pp. (in Russian)

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

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