Построение и верификация LD-программ ПЛК по LTL-спецификации

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

1. Кузьмин Е. В., Соколов В. А., Рябухин Д. А. Построение и верификация ПЛК-программ по 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]).

2. Кузьмин Е. В., Рябухин Д. А., Шипов А. А. Построение и верификация ПЛК-программ по 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]).

3. Кузьмин Е. В., Соколов В. А. Моделирование, спецификация и построение программ логических контроллеров // Моделирование и анализ информационных систем. 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]).

4. Кузьмин Е. В., Соколов В. А. О построении и верификации программ логических контроллеров // Моделирование и анализ информационных систем. 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]).

5. Кузьмин Е. В., Соколов В. А. О верификации 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]).

6. Петров И. В. Программируемые контроллеры. Стандартные языки и приемы прикладного проектирования. М.: СОЛОН-Пресс, 2004. 256 с. (Petrov I. V. Programmiruemye kontrollery. Standartnye jazyki i priemy prikladnogo proektirovanija. M.: SOLONPress, 2004. 256 p. [in Russian]).

7. Clark E. M., Grumberg O., Peled D. A. Model Checking. The MIT Press, 2001.

8. CoDeSys. Controller Development System. http://www.3s-software.com/

9. Parr E. A. Programmable Controllers. An engineer’s guide. Newnes, 2003. 442 p.

10. SMV. The Cadence SMV Model Checker. http://www.kenmcmil.com/smv.html