Construction of CFC-programs by LTL-specification
https://doi.org/10.18255/1818-1015-2016-2-173-184
Abstract
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-, LDand 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.
About the Authors
D. A. Ryabukhin
P.G. Demidov Yaroslavl State University,
Sovetskaya str., 14, Yaroslavl, 150000, Russia
Russian Federation
Russian Federation
graduate student
E. V. Kuzmin
P.G. Demidov Yaroslavl State University,
Sovetskaya str., 14, Yaroslavl, 150000, Russia
Russian Federation
Russian Federation
doctor of science, associate professor
V. A. Sokolov
P.G. Demidov Yaroslavl State University,
Sovetskaya str., 14, Yaroslavl, 150000, Russia
Russian Federation
Russian Federation
doctor of science, professor
References
1. Кузьмин Е.В., Рябухин Д.А., Соколов В.А., “О выразительности подхода к построению ПЛК-программ по LTL-спецификации”, Моделирование и анализ информационных систем, 22:4 (2015), 507–520; [Kuzmin E. V., Ryabukhin D. A., Sokolov V. A., “On the Expressiveness of the Approach to Constructing PLC-programs by LTLSpecification”, Modeling and Analysis of Information Systems, 22:4 (2015), 507–520, (in Russian).]
2. КузьминЕ.В.,РябухинД.А.,СоколовВ.А.,“Моделированиесогласованногоповедения ПЛК-датчиков”, Моделирование и анализ информационных систем, 21:4 (2014), 75–90; [KuzminE.V.,RyabukhinD.A.,SokolovV.A.,“ModelingaConsistentBehavior of PLC-Sensors”, Modeling and Analysis of Information Systems, 21:4 (2014), 75–90, (in Russian).]
3. Рябухин Д. А., Кузьмин Е. В., Соколов В. А., “ Построение IL-программ ПЛК по LTLспецификации”, Моделиров. и анализ информационных систем, 21:2 (2014), 26–38; [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).]
4. Кузьмин Е. В., Соколов В. А., Рябухин Д. А., “ Построение и верификация LDпрограмм ПЛК по LTL-спецификации”, Моделирование и анализ информационных систем,20:6(2013),78–94; [KuzminE.V.,SokolovV.A.,RyabukhinD.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. Кузьмин Е.В., Соколов В.А., Рябухин Д.А., “Построение и верификация ПЛКпрограмм по LTL-спецификации”, Моделирование и анализ информационных систем, 20:4 (2013), 5–22; [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).]
6. КузьминЕ.В.,СоколовВ.А.,“Моделирование,спецификацияипостроениепрограмм логических контроллеров”, Моделирование и анализ информационных систем, 20:2 (2013), 104–120; [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.
8. Clark E. M., Grumberg O., Peled D. A., Model Checking, The MIT Press, 2001.
9. CoDeSys, Controller Development System, http://www.3s-software.com/.
10. Kuzmin E.V., Sokolov V.A., Ryabukhin D.A., “Construction and Verification of PLCPrograms by LTL-Specification”, Automatic Control and Computer Sciences, 49:7 (2015), 453–465.
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.
12. KuzminE.V.,SokolovV.A.,“Modeling,SpecificationandConstructionofPLC-programs”, Automatic Control and Computer Sciences, 48:7 (2014), 554–563.
13. Kuzmin E.V., Ryabukhin D.A., Sokolov V.A., “Modeling a Consistent Behavior of PLCSensors”, Automatic Control and Computer Sciences, 48:7 (2014), 602–614.
14. SMV, The Cadence SMV Model Checker, 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. PakonenA.,MatasniemiT.,LahtinenJ.,KarhelaT.,“AtoolsetformodelcheckingofPLC 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. Петров И.В., Программируемые контроллеры. Стандартные языки и приемы прикладного проектирования, М.: СОЛОН-Пресс, 2004; [Petrov I.V., Programmiruemye kontrollery. Standartnye jazyki i priemy prikladnogo proektirovanija, M.: SOLON-Press, 2004, (in Russian).]
Review
For citations:
Ryabukhin D.A., Kuzmin E.V., Sokolov V.A. Construction of CFC-programs by LTL-specification. Modeling and Analysis of Information Systems. 2016;23(2):173-184. (In Russ.) https://doi.org/10.18255/1818-1015-2016-2-173-184
Views:
1421
Email this article 