Geodesic
Construction of CFC-programs by LTL-specification
Modelirovanie i analiz informacionnyh sistem, Tome 23 (2016) no. 2, pp. 173-184.

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

This article continues a cycle of papers, which describe an approach to construction and verification of discrete PLC-programs by an LTL-specification. The approach provides a possibility of PLC-program correctness analysis by the model checking method. For the specification of the program behavior the linear-time temporal logic LTL is used. The correctness analysis of an LTL specification is performed automatically by the symbolic model checking tool Cadence SMV. Previously it was shown how ST-, LD- and IL-programs are constructed by a correct (with verified program properties) LTL-specification. In this article a technology of CFC-program construction by an LTL-specification is described. The language CFC (Continuous Function Chart) is a variation of FBD (Function Block Diagram). FBD is a graphical language for microcircuits. CFC provides a possibility of free allocation of program components and connections on a screen. The approach to construction of CFC-programs is shown by an example. PLC-program representation on CFC within the approach to programming by LTL-specification differs from other representations. It gives the visualisation of a data flow from inputs to outputs. Influence and dependence between variables is explicitly shown during program execution within one PLC working cycle. In fact, CFC-program is a scheme of PLC-program data flow.
Keywords: programmable logic controllers (PLC), construction and verification of PLC-programs, LTL-specification, CFC-diagrams. 
@article{MAIS_2016_23_2_a5,
     author = {D. A. Ryabukhin and E. V. Kuzmin and V. A. Sokolov},
     title = {Construction of {CFC-programs} by {LTL-specification}},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {173--184},
     publisher = {mathdoc},
     volume = {23},
     number = {2},
     year = {2016},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2016_23_2_a5/}
}
TY  - JOUR
AU  - D. A. Ryabukhin
AU  - E. V. Kuzmin
AU  - V. A. Sokolov
TI  - Construction of CFC-programs by LTL-specification
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2016
SP  - 173
EP  - 184
VL  - 23
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2016_23_2_a5/
LA  - ru
ID  - MAIS_2016_23_2_a5
ER  - 
%0 Journal Article
%A D. A. Ryabukhin
%A E. V. Kuzmin
%A V. A. Sokolov
%T Construction of CFC-programs by LTL-specification
%J Modelirovanie i analiz informacionnyh sistem
%D 2016
%P 173-184
%V 23
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2016_23_2_a5/
%G ru
%F MAIS_2016_23_2_a5
D. A. Ryabukhin; E. V. Kuzmin; V. A. Sokolov. Construction of CFC-programs by LTL-specification. Modelirovanie i analiz informacionnyh sistem, Tome 23 (2016) no. 2, pp. 173-184. http://geodesic.mathdoc.fr/item/MAIS_2016_23_2_a5/

[1] Kuzmin E. V., Ryabukhin D. A., Sokolov V. A., “On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification”, Modeling and Analysis of Information Systems, 22:4 (2015), 507–520 (in Russian) | MR

[2] Kuzmin E. V., Ryabukhin D. A., Sokolov V. A., “Modeling a Consistent Behavior of PLC-Sensors”, Modeling and Analysis of Information Systems, 21:4 (2014), 75–90 (in Russian) | MR

[3] 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

[4] 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)

[5] 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

[6] 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)

[7] Baier C., Katoen J.-P., Principles of Model Checking, The MIT Press, 2008 | MR

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

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

[10] Kuzmin E. V., Sokolov V. A., Ryabukhin D. A., “Construction and Verification of PLC-Programs by LTL-Specification”, Automatic Control and Computer Sciences, 49:7 (2015), 453–465 | DOI

[11] Kuzmin E. V., Sokolov V. A., Ryabukhin D. A., “Construction and Verification of PLC LD Programs by the LTL Specification”, Automatic Control and Computer Sciences, 48:7 (2014), 424–436 | DOI

[12] Kuzmin E. V., Sokolov V. A., “Modeling, Specification and Construction of PLC-programs”, Automatic Control and Computer Sciences, 48:7 (2014), 554–563 | DOI

[13] Kuzmin E. V., Ryabukhin D. A., Sokolov V. A., “Modeling a Consistent Behavior of PLC-Sensors”, Automatic Control and Computer Sciences, 48:7 (2014), 602–614 | DOI

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

[15] Wardana A., Development of Automatic Program Verification for Continious Function Chart based on Model Checking, Kassel university press GmbH

[16] Ovataman T., Aral A., Polat D., Unver A. O., “An overview of model checking practices on verification of PLC software”, Software and Systems Modeling, 2014

[17] Pakonen A., Matasniemi T., Lahtinen J., Karhela T., “A toolset for model checking of PLC software”, Proceedings of 18th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA2013 (Cagliari, Italy, 2013)

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

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