maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2014-2-26-38mais-117Research ArticleОригинальные статьиArticlesПостроение IL-программ ПЛК по LTL-спецификацииConstruction of PLC IL-Programs by LTL-SpecificationРябухинДмитрий АлександровичRyabukhinD. A.

аспирант,

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

аспирант,

Sovetskaya str., 14, Yaroslavl, 150000, Russia

dmitriy_ryabukhin@mail.ruКузьминЕгор ВладимировичKuzminE. V.

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

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

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

Sovetskaya str., 14, Yaroslavl, 150000, Russia

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

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

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

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

Sovetskaya str., 14, Yaroslavl, 150000, Russia

 

sokolov@uniyar.ac.ruЯрославский государственный университет им. П. Г. ДемидоваРоссияP.G. Demidov Yaroslavl State UniversityRussian Federation2014200420142122638Copyright © Рябухин Д.А., Кузьмин Е.В., Соколов В.А., 20142014Рябухин Д.А., Кузьмин Е.В., Соколов В.А.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/117

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

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

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

An approach to the construction and verification of PLC IL-programs for discrete problems is proposed. For the specification of the program behavior, we use the linear-time temporal logic LTL. Programming is carried out in the IL-language (Instruction List) 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 PLC IL-programs is shown by an example. For a discrete problem, we give an IL-program and its LTL-specification.

The purpose of the article is to describe an approach to programming PLC, which would provide a possibility of IL-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 which 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 speci- fication of the corresponding variable behavior) are constructive in the sense that they construct the PLC-program (IL-program), which satisfies temporal properties expressed by these formulas. Thus, the programming of PLC is reduced to the construction of LTLspecification of the behavior of each program variable. In addition, an SMV-model of a PLC IL-program is constructed according to LTL-specification. Then, the SMV-model is analysed by the symbolic model checking tool Cadence SMV.

программируемые логические контроллерытехнология программированияспецификация и верификация программсписок инструкцийprogrammable logic controllerssoftware engineeringspecification and verification of PLC-programsInstruction ListРФФИReferencesКузьмин Е. В., Соколов В. А., Рябухин Д. А. Построение и верификация LD-программ ПЛК по LTL-спецификации // Моделирование и анализ информационных систем. Ярославль, 2013. Т. 20, №6 (2013). С. 78–94. [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. 2013. V. 20, №6. P. 78–94 (in Russian)].Кузьмин Е. В., Соколов В. А., Рябухин Д. А. Построение и верификация LD-программ ПЛК по LTL-спецификации // Моделирование и анализ информационных систем. Ярославль, 2013. Т. 20, №6 (2013). С. 78–94. [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. 2013. V. 20, №6. P. 78–94 (in Russian)].Кузьмин Е. В., Соколов В. А., Рябухин Д. А. Построение и верификация ПЛК-программ по LTL-спецификации // Моделирование и анализ информационных систем. 2013. Т. 20, №4. С. 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. 2013. V. 20, №4. P. 5–22 (in Russian)].Кузьмин Е. В., Соколов В. А., Рябухин Д. А. Построение и верификация ПЛК-программ по LTL-спецификации // Моделирование и анализ информационных систем. 2013. Т. 20, №4. С. 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. 2013. V. 20, №4. P. 5–22 (in Russian)].Кузьмин Е. В., Рябухин Д. А., Шипов А. А. Построение и верификация ПЛК-программ по LTL-спецификации // Международная научно-практическая конференция «Инструменты и методы анализа программ». Кострома, КГТУ, 2013. С. 17–34. [Kuzmin E. V., Ryabukhin D. A., Shipov A. A. Construction and Verification of PLCprograms by LTL-specification // Proc. of Int. Conf. «Tools and Methods of Program Analysis (TMPA-2013)». Kostroma, KSTU, 2013. P. 17–34 (in Russian)].Кузьмин Е. В., Рябухин Д. А., Шипов А. А. Построение и верификация ПЛК-программ по LTL-спецификации // Международная научно-практическая конференция «Инструменты и методы анализа программ». Кострома, КГТУ, 2013. С. 17–34. [Kuzmin E. V., Ryabukhin D. A., Shipov A. A. Construction and Verification of PLCprograms by LTL-specification // Proc. of Int. Conf. «Tools and Methods of Program Analysis (TMPA-2013)». Kostroma, KSTU, 2013. P. 17–34 (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)].Кузьмин Е. В., Соколов В. А. Моделирование, спецификация и построение программ логических контроллеров // Моделирование и анализ информационных систем. 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 LD-Language // 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 LD-Language // 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)].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/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.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.