Geodesic
Modeling a Consistent Behavior of PLC-Sensors
Modelirovanie i analiz informacionnyh sistem, Tome 21 (2014) no. 4, pp. 75-90.

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

The article extends the cycle of papers dedicated to programming and verificatoin of PLC-programs by LTL-specification. This approach provides the availability of correctness analysis of PLC-programs by the model checking method. The model checking method needs to construct a finite model of a PLC program. For successful verification of required properties it is important to take into consideration that not all combinations of input signals from the sensors can occur while PLC works with a control object. This fact requires more advertence to the construction of the PLC-program model. In this paper we propose to describe a consistent behavior of sensors by three groups of LTL-formulas. They will affect the program model, approximating it to the actual behavior of the PLC program. The idea of LTL-requirements is shown by an example. A PLC program is a description of reactions on input signals from sensors, switches and buttons. In constructing a PLC-program model, the approach to modeling a consistent behavior of PLC sensors allows to focus on modeling precisely these reactions without an extension of the program model by additional structures for realization of a realistic behavior of sensors. The consistent behavior of sensors is taken into account only at the stage of checking a conformity of the programming model to required properties, i. e. a property satisfaction proof for the constructed model occurs with the condition that the model contains only such executions of the program that comply with the consistent behavior of sensors.
Keywords: programmable logic controllers, software engineering, specification and verification of PLC-programs, sensor modeling. 
@article{MAIS_2014_21_4_a7,
     author = {E. V. Kuzmin and D. A. Ryabukhin and V. A. Sokolov},
     title = {Modeling a {Consistent} {Behavior} of {PLC-Sensors}},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {75--90},
     publisher = {mathdoc},
     volume = {21},
     number = {4},
     year = {2014},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2014_21_4_a7/}
}
TY  - JOUR
AU  - E. V. Kuzmin
AU  - D. A. Ryabukhin
AU  - V. A. Sokolov
TI  - Modeling a Consistent Behavior of PLC-Sensors
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2014
SP  - 75
EP  - 90
VL  - 21
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2014_21_4_a7/
LA  - ru
ID  - MAIS_2014_21_4_a7
ER  - 
%0 Journal Article
%A E. V. Kuzmin
%A D. A. Ryabukhin
%A V. A. Sokolov
%T Modeling a Consistent Behavior of PLC-Sensors
%J Modelirovanie i analiz informacionnyh sistem
%D 2014
%P 75-90
%V 21
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2014_21_4_a7/
%G ru
%F MAIS_2014_21_4_a7
E. V. Kuzmin; D. A. Ryabukhin; V. A. Sokolov. Modeling a Consistent Behavior of PLC-Sensors. Modelirovanie i analiz informacionnyh sistem, Tome 21 (2014) no. 4, pp. 75-90. http://geodesic.mathdoc.fr/item/MAIS_2014_21_4_a7/

[1] Ryabukhin D. A., Kuzmin E. V., Sokolov V. A., “Construction of PLC IL-programs by LTL-specification”, Modeling and analysis of information systems, 21:2 (2014), 26–38 (in Russian) | MR

[2] Kuzmin E. V., Sokolov V. A., Ryabukhin D. A., “Construction and Verification of PLC LD-programs by LTL-specification”, Modeling and analysis of information systems, 20:6 (2013), 78–94 (in Russian)

[3] Kuzmin E. V., Sokolov V. A., Ryabukhin D. A., “Construction and Verification of PLC-programs by LTL-specification”, Modeling and analysis of information systems, 20:4 (2013), 5–22 (in Russian) | MR

[4] Kuzmin E. V., Ryabukhin D. A., Shipov A. A., “Construction and Verification of PLC-programs by LTL-specification”, Proc. of Int. Conf. «Tools and Methods of Program Analysis», TMPA-2013 (Kostroma, 2013), 17–34 (in Russian)

[5] Kuzmin E. V., Sokolov V. A., “Modeling, Specification and Construction of PLC-programs”, Modeling and analysis of information systems, 20:2 (2013), 104–120 (in Russian)

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

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

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

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

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