Построение CFC-программ ПЛК по LTL-спецификации
https://doi.org/10.18255/1818-1015-2016-2-173-184
Аннотация
Статья продолжает серию работ, посвященных подходу к построению и верификации «дискретных» программ логических контроллеров (ПЛК) по 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-программа представляет собой схему потоков данных ПЛК-программы.
Об авторах
Д. А. Рябухин
Ярославский государственный университет им. П.Г. Демидова
Россия
Россия
аспирант
Е. В. Кузьмин
Ярославский государственный университет им. П.Г. Демидова
Россия
Россия
доктор физ.-мат. наук, доцент, профессор кафедры теоретической информатики
В. А. Соколов
Ярославский государственный университет им. П.Г. Демидова
Россия
Россия
доктор физ.-мат. наук, профессор, зав. кафедрой теоретической информатики
Список литературы
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).]
Рецензия
Для цитирования:
Рябухин Д.А., Кузьмин Е.В., Соколов В.А. Построение CFC-программ ПЛК по LTL-спецификации. Моделирование и анализ информационных систем. 2016;23(2):173-184. https://doi.org/10.18255/1818-1015-2016-2-173-184
For citation:
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
Просмотров: 1172
Послать статью по эл. почте 