maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2013-4-5-22mais-181Research ArticleОригинальные статьиArticlesПостроение и верификация ПЛК-программ по LTL-спецификацииConstruction and Verification of PLC-programs by LTL-specificationКузьминЕгор ВладимировичKuzminE. V.

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

150000 Россия, г. Ярославль, ул. Советская, 14

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

Sovetskaya str., 14, Yaroslavl, 150000, Russia

kuzmin@uniyar.ac.ruСоколовВалерий АнатольевичSokolovV. A.

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

150000 Россия, г. Ярославль, ул. Советская, 14

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

Sovetskaya str., 14, Yaroslavl, 150000, Russia

sokolov@uniyar.ac.ruРябухинДмитрий АлександровичRyabukhinD. A.

аспирант,

150000 Россия, г. Ярославль, ул. Советская, 14

аспирант,

Sovetskaya str., 14, Yaroslavl, 150000, Russia

dmitriy_ryabukhin@mail.ruЯрославский государственный университет им. П. Г. ДемидоваРоссияP.G. Demidov Yaroslavl State UniversityRussian Federation201320082013204522Copyright © Кузьмин Е.В., Соколов В.А., Рябухин Д.А., 20132013Кузьмин Е.В., Соколов В.А., Рябухин Д.А.Kuzmin E.V., Sokolov V.A., Ryabukhin D.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/181

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

Целью статьи является описание подхода к программированию ПЛК, который бы обеспечивал возможность анализа корректности ПЛК-программ с помощью метода проверки модели.

Поэтому изменение значения каждой программной переменной описывается с помощью пары LTL-формул. Первая LTL-формула описывает ситуации, при которых происходит возрастание значения соответствующей переменной, вторая LTL-формула задает условия, приводящие к уменьшению значения переменной. Рассматриваемые для спецификации поведения переменных LTL- формулы являются конструктивными в том смысле, что по ним производится построение ПЛК-программы, которая соответствует темпоральным свойствам, выраженным этими формулами. Таким образом, программирование ПЛК сводится к построению LTL-спецификации поведения каждой программной переменной. Кроме этого, по LTL-спецификации строится SMV-модель, которая затем проверяется на корректность (относительно дополнительных общепро- граммных LTL-свойств) методом проверки модели с помощью средства верификации Cadence SMV.

An approach to construction and verification of PLC-programs for discrete tasks is proposed. For the specification of a program behavior we use the linear-time temporal logic LTL. Programming is carried out in the ST-language according to an LTL-specification. The correctness analysis of an LTL-specification is carried out by the symbolic model checking tool Cadence SMV. A new approach to programming and verification of PLCprograms is shown by an example. For a discrete problem we give a ST-program, its LTL-specification and an SMV-model.

A purpose of the article is to describe an approach to programming PLC, which would provide a possibility of PLC-program correctness analysis by the model checking method.

Under the proposed approach the change of the value of each program variable is described by a pair of LTL-formulas. The first LTL-formula describes situations that increase the value of the corresponding variable, the second LTL-formula specifies conditions leading to a decrease of the variable value. The LTL-formulas (used for specification of the corresponding variable behavior) are constructive in the sense that they construct the PLC-program, which satisfies temporal properties expressed by these formulas. Thus, the programming of PLC is reduced to the construction of LTL-specification of the behavior of each program variable. In addition, an SMV-model of a PLC-program is constructed according to LTL-specification. Then, the SMV-model is analysed by the symbolic model checking tool Cadence SMV.

программируемые логические контроллерытехнология программированияспецификация и верификация программprogrammable pogic controllerssoftware engineeringspecification and verification of PLC-programsРФФИ, Минобрнауки РФ, ФЦП "Научные и научно-педагогические кадры инновационной России" на 2009–2013 годыReferencesКузьмин Е. В., Соколов В. А. Моделирование, спецификация и построение программ логических контроллеров // Моделирование и анализ информационных систем. 2013. Т. 20, №2. С. 104–120. (Kuzmin E. V., Sokolov V. A. Modeling, Specification and Construction of PLC-programs // Modeling and analysis of information systems. 2013. V. 20, №2. P. 104–120 [in Russian]).Кузьмин Е. В., Соколов В. А. Моделирование, спецификация и построение программ логических контроллеров // Моделирование и анализ информационных систем. 2013. Т. 20, №2. С. 104–120. (Kuzmin E. V., Sokolov V. A. Modeling, Specification and Construction of PLC-programs // Modeling and analysis of information systems. 2013. V. 20, №2. P. 104–120 [in Russian]).Кузьмин Е. В., Соколов В. А. О построении и верификации программ логических контроллеров // Моделирование и анализ информационных систем. 2012. Т. 19, №4. С. 25–36. (Kuzmin E. V., Sokolov V. A. On Construction and Verification of PLC-Programs // Modeling and analysis of information systems. 2012. V. 19, №4. P. 25–36 [in Russian]).Кузьмин Е. В., Соколов В. А. О построении и верификации программ логических контроллеров // Моделирование и анализ информационных систем. 2012. Т. 19, №4. С. 25–36. (Kuzmin E. V., Sokolov V. A. On Construction and Verification of PLC-Programs // Modeling and analysis of information systems. 2012. V. 19, №4. P. 25–36 [in Russian]).Кузьмин Е. В., Соколов В. А. О верификации LD-программ логических контроллеров // Моделирование и анализ информационных систем. 2012. Т. 19, №2. С. 138–144. (Kuzmin E. V., Sokolov V. A. On Verification of PLC-Programs Written in the LDLanguage // Modeling and analysis of information systems. 2012. V. 19, №2. P. 138–144 [in Russian]).Кузьмин Е. В., Соколов В. А. О верификации LD-программ логических контроллеров // Моделирование и анализ информационных систем. 2012. Т. 19, №2. С. 138–144. (Kuzmin E. V., Sokolov V. A. On Verification of PLC-Programs Written in the LDLanguage // Modeling and analysis of information systems. 2012. V. 19, №2. P. 138–144 [in Russian]).Петров И. В. Программируемые контроллеры. Стандартные языки и приемы прикладного проектирования. М.: СОЛОН-Пресс, 2004. 256 с. (Petrov I. V. Programmiruemye kontrollery. Standartnye jazyki i priemy prikladnogo proektirovanija. M.: SOLONPress, 2004. 256 p. [in Russian]).Петров И. В. Программируемые контроллеры. Стандартные языки и приемы прикладного проектирования. М.: СОЛОН-Пресс, 2004. 256 с. (Petrov I. V. Programmiruemye kontrollery. Standartnye jazyki i priemy prikladnogo proektirovanija. M.: SOLONPress, 2004. 256 p. [in Russian]).Canet G., Couffin S., Lesage J.-J., Petit A., Schnoebelen Ph. Towards the Automatic Verification of PLC Programs Written in Instruction List // Proc. of the IEEE International Conference on Systems, Man and Cybernetics. Argos Press, 2000. P. 2449–2454.Canet G., Couffin S., Lesage J.-J., Petit A., Schnoebelen Ph. Towards the Automatic Verification of PLC Programs Written in Instruction List // Proc. of the IEEE International Conference on Systems, Man and Cybernetics. Argos Press, 2000. P. 2449–2454.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/Gries D. The Science of Programming. Springer-Verlag, 1981.Gries D. The Science of Programming. Springer-Verlag, 1981.Parr E. A. Programmable Controllers. An engineer’s guide. Newnes, 2003. 442 p.Parr E. A. Programmable Controllers. An engineer’s guide. Newnes, 2003. 442 p.Pavlovic O., Pinger R., Kollmann M. Automation of Formal Verification of PLC Programs Written in IL // Proceedings of 4th International Verification Workshop (VERIFY’07). Bremen, Germany, 2007. P. 152–163.Pavlovic O., Pinger R., Kollmann M. Automation of Formal Verification of PLC Programs Written in IL // Proceedings of 4th International Verification Workshop (VERIFY’07). Bremen, Germany, 2007. P. 152–163.Rossi O., Schnoebelen Ph. Formal Modeling of Timed Function Blocks for the Automatic Verification of Ladder Diagram Programs // Proc. of the 4th International Conference on Automation of Mixed Processes: Hybrid Dynamic Systems, Shaker Verlag, 2000. P. 177-182.Rossi O., Schnoebelen Ph. Formal Modeling of Timed Function Blocks for the Automatic Verification of Ladder Diagram Programs // Proc. of the 4th International Conference on Automation of Mixed Processes: Hybrid Dynamic Systems, Shaker Verlag, 2000. P. 177-182.SMV. The Cadence SMV Model Checker. http://www.kenmcmil.com/smv.htmlSMV. The Cadence SMV Model Checker. http://www.kenmcmil.com/smv.html

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