maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2013-2-104-120mais-209Research ArticleОригинальные статьиArticlesМоделирование, спецификация и построение программ логических контроллеровModeling, Specification and Construction of PLC-programsКузьминЕгор Владимирович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Ярославский государственный университет им. П.Г. ДемидоваРоссияP.G. Demidov Yaroslavl State UniversityRussian Federation201320042013202104120Copyright © Кузьмин Е.В., Соколов В.А., 20132013Кузьмин Е.В., Соколов В.А.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/209

Предлагается новый подход к построению надежных «дискретных» ПЛК-программ с таймерами — программирование исходя из задач спецификации и верификации. Для спецификации программного поведения используется язык темпоральной логики LTL. Программирование осуществляется на языке ST по LTL-спецификации. Проводится дискретное моделирование таймера. Новый подход к программированию ПЛК демонстрируется на примере.

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

1) значение каждой переменной должно изменяться не более одного раза за одно полное выполнение программы при прохождении рабочего цикла ПЛК;

2) значение каждой переменной должно изменяться только в одном месте про- граммы ПЛК.

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

A new approach to construction of reliable discrete PLC-programs with timers — programming based on specification and verification — is proposed. Timers are modelled in a discrete way. 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 a LTLspecification. A new approach to programming of PLC is shown by an example. The proposed programming approach provides an ability of a correctness analysis of PLC-programs using the model checking method. The programming requires fulfillment of the following two conditions: 1) a value of each variable should be changed not more than once per one full PLC-program implementation (per one full working cycle of PLC); 2) a value of each variable should only be changed in one place of a PLC-program. 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.

программируемые логические контроллерытехнология программированиямоделирование и спецификация программprogrammable pogic controllerssoftware engineeringmodeling and specification of PLC-programsРФФИ, Минобрнауки РФ, ФЦП "Научные и научно-педагогические кадры инновационной России" на 2009–2013 годыReferencesГрис Д. Наука программирования: Пер. с англ. М.: Мир, 1984. 416 с. (Gries D. The Science of Programming. Springer-Verlag, 1981).Грис Д. Наука программирования: Пер. с англ. М.: Мир, 1984. 416 с. (Gries D. The Science of Programming. Springer-Verlag, 1981).Кларк Э. М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking: Пер. с англ. М.: МЦНМО, 2002. 416 с. (Clark E. M., Grumberg O., Peled D. A. Model Checking. The MIT Press, 2001).Кларк Э. М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking: Пер. с англ. М.: МЦНМО, 2002. 416 с. (Clark E. M., Grumberg O., Peled D. A. Model Checking. The MIT Press, 2001).Кузьмин Е. В., Соколов В. А. О построении и верификации программ логических контроллеров // Моделирование и анализ информационных систем. 2012. Т. 19, №4. С. 25–36 (Kuzmin E. V., Sokolov V. A. On Construction and Verification of PLCPrograms // 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 PLCPrograms // 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]).Парр Э. Программируемые контроллеры: руководство для инженера. М.: БИНОМ. Лаборатория знаний, 2007. 516 с. (Parr E. A. Programmable Controllers. An engineer’s guide. Newnes, 2003. 442 p.).Парр Э. Программируемые контроллеры: руководство для инженера. М.: БИНОМ. Лаборатория знаний, 2007. 516 с. (Parr E. A. Programmable Controllers. An engineer’s guide. Newnes, 2003. 442 p.).Петров И. В. Программируемые контроллеры. Стандартные языки и приемы прикладного проектирования. М.: СОЛОН-Пресс, 2004. 256 с. (Petrov I. V. Programmiruemye kontrollery. Standartnye jazyki i priemy prikladnogo proektirovanija. M.: SOLON-Press, 2004. 256 p. [in Russian]).Петров И. В. Программируемые контроллеры. Стандартные языки и приемы прикладного проектирования. М.: СОЛОН-Пресс, 2004. 256 с. (Petrov I. V. Programmiruemye kontrollery. Standartnye jazyki i priemy prikladnogo proektirovanija. M.: SOLON-Press, 2004. 256 p. [in Russian]).CoDeSys. Controller Development System. http://www.3s-software.com/CoDeSys. Controller Development System. http://www.3s-software.com/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.