maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2016-2-173-184mais-327Research ArticleОригинальные статьиArticlesПостроение CFC-программ ПЛК по LTL-спецификацииConstruction of CFC-programs by LTL-specificationРябухинД. А.RyabukhinD. A.

аспирант

graduate student

dmitriy_ryabukhin@mail.ruКузьминЕ. В.KuzminE. V.

доктор физ.-мат. наук, доцент, профессор кафедры теоретической информатики

doctor of science, associate professor

kuzmin@uniyar.ac.ruСоколовВ. А.SokolovV. A.

доктор физ.-мат. наук, профессор, зав. кафедрой теоретической информатики

doctor of science, professor

sokolov@uniyar.ac.ruЯрославский государственный университет им. П.Г. ДемидоваРоссияP.G. Demidov Yaroslavl State University,
Sovetskaya str., 14, Yaroslavl, 150000, RussiaRussian Federation201620042016232173184Copyright © Рябухин Д.А., Кузьмин Е.В., Соколов В.А., 20162016Рябухин Д.А., Кузьмин Е.В., Соколов В.А.Ryabukhin D.A., Kuzmin E.V., Sokolov V.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/327

Статья продолжает серию работ, посвященных подходу к построению и верификации «дискретных» программ логических контроллеров (ПЛК) по LTL-спецификации. Этот подход обеспечивает возможность анализа корректности программ логических контроллеров с помощью метода проверки модели (Model Checking). В рамках подхода в качестве языка спецификации программного поведения используется язык темпоральной логики LTL. Анализ корректности LTL-спецификации относительно программных свойств производится автоматически с помощью программного средства символьной проверки модели Cadence SMV. 

Ранее было показано, каким образом по корректной (проверенной на корректность относительно программных свойств) LTL-спецификации происходит построение ST-, LDи IL-программ. В этой статье описывается технология построения CFC-программ по LTL-спецификации. Язык непрерывных функциональных схем CFC (Continuous Function Chart) представляет собой разновидность языка FBD (Function Block Diagram) — графического языка диаграмм принципиальных схем электронных устройств на микросхемах. В отличие от FBD язык CFC обеспечивает возможность свободного размещения программных компонентов и их соединений на экране. Технология построения CFC-программ демонстрируется на примере. 

Представление ПЛК-программы на языке CFC в рамках подхода к программированию по LTL-спецификации в отличие от представлений на других стандартных языках дает возможность наглядного графического изображения потока данных от входных переменных к выходам ПЛК. Явным образом демонстрируется зависимость и влияние значений одних переменных на значения других переменных во время исполнения программы за один проход рабочего цикла ПЛК. Фактически CFC-программа представляет собой схему потоков данных ПЛК-программы. 

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.

программируемые логические контроллеры (ПЛК)построение и верификация ПЛК-программLTL-спецификацияCFC-диаграммыprogrammable logic controllers (PLC)construction and verification of PLC-programsLTL-specificationCFC-diagramsReferencesКузьмин Е.В., Рябухин Д.А., Соколов В.А., “О выразительности подхода к построению ПЛК-программ по 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).]Кузьмин Е.В., Рябухин Д.А., Соколов В.А., “О выразительности подхода к построению ПЛК-программ по 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).]КузьминЕ.В.,РябухинД.А.,СоколовВ.А.,“Моделированиесогласованногоповедения ПЛК-датчиков”, Моделирование и анализ информационных систем, 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).]КузьминЕ.В.,РябухинД.А.,СоколовВ.А.,“Моделированиесогласованногоповедения ПЛК-датчиков”, Моделирование и анализ информационных систем, 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).]Рябухин Д. А., Кузьмин Е. В., Соколов В. А., “ Построение 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).]Рябухин Д. А., Кузьмин Е. В., Соколов В. А., “ Построение 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).]Кузьмин Е. В., Соколов В. А., Рябухин Д. А., “ Построение и верификация 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).]Кузьмин Е. В., Соколов В. А., Рябухин Д. А., “ Построение и верификация 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).]Кузьмин Е.В., Соколов В.А., Рябухин Д.А., “Построение и верификация ПЛКпрограмм по 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).]Кузьмин Е.В., Соколов В.А., Рябухин Д.А., “Построение и верификация ПЛКпрограмм по 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).]КузьминЕ.В.,СоколовВ.А.,“Моделирование,спецификацияипостроениепрограмм логических контроллеров”, Моделирование и анализ информационных систем, 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).]КузьминЕ.В.,СоколовВ.А.,“Моделирование,спецификацияипостроениепрограмм логических контроллеров”, Моделирование и анализ информационных систем, 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).]Baier C., Katoen J.-P., Principles of Model Checking, The MIT Press, 2008.Baier C., Katoen J.-P., Principles of Model Checking, The MIT Press, 2008.Clark E. M., Grumberg O., Peled D. A., Model Checking, The MIT Press, 2001.Clark E. M., Grumberg O., Peled D. A., Model Checking, The MIT Press, 2001.CoDeSys, Controller Development System, http://www.3s-software.com/.CoDeSys, Controller Development System, http://www.3s-software.com/.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.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.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.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.KuzminE.V.,SokolovV.A.,“Modeling,SpecificationandConstructionofPLC-programs”, Automatic Control and Computer Sciences, 48:7 (2014), 554–563.KuzminE.V.,SokolovV.A.,“Modeling,SpecificationandConstructionofPLC-programs”, Automatic Control and Computer Sciences, 48:7 (2014), 554–563.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.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.SMV, The Cadence SMV Model Checker, http://www.kenmcmil.com/smv.html.SMV, The Cadence SMV Model Checker, http://www.kenmcmil.com/smv.html.Wardana A., Development of Automatic Program Verification for Continious Function Chart based on Model Checking, Kassel university press GmbH.Wardana A., Development of Automatic Program Verification for Continious Function Chart based on Model Checking, Kassel university press GmbH.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.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.PakonenA.,MatasniemiT.,LahtinenJ.,KarhelaT.,“AtoolsetformodelcheckingofPLC software”, Proceedings of 18th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA2013, Cagliari, Italy, 2013.PakonenA.,MatasniemiT.,LahtinenJ.,KarhelaT.,“AtoolsetformodelcheckingofPLC software”, Proceedings of 18th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA2013, Cagliari, Italy, 2013.Parr E. A., Programmable Controllers. An engineer’s guide, Newnes, 2003.Parr E. A., Programmable Controllers. An engineer’s guide, Newnes, 2003.Петров И.В., Программируемые контроллеры. Стандартные языки и приемы прикладного проектирования, М.: СОЛОН-Пресс, 2004; [Petrov I.V., Programmiruemye kontrollery. Standartnye jazyki i priemy prikladnogo proektirovanija, M.: SOLON-Press, 2004, (in Russian).]Петров И.В., Программируемые контроллеры. Стандартные языки и приемы прикладного проектирования, М.: СОЛОН-Пресс, 2004; [Petrov I.V., Programmiruemye kontrollery. Standartnye jazyki i priemy prikladnogo proektirovanija, M.: SOLON-Press, 2004, (in Russian).]

The authors declare that there are no conflicts of interest present.