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.
@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},
year = {2013},
volume = {20},
number = {2},
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
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
%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)
