Preview

Моделирование и анализ информационных систем

Расширенный поиск

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

https://doi.org/10.18255/1818-1015-2013-6-78-94

Аннотация

Предлагается подход к построению и верификации 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.

Об авторах

Егор Владимирович Кузьмин
Ярославский государственный университет им. П. Г. Демидова
Россия

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

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



Валерий Анатольевич Соколов
Ярославский государственный университет им. П. Г. Демидова
Россия

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

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



Дмитрий Александрович Рябухин
Ярославский государственный университет им. П. Г. Демидова
Россия

аспирант,

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



Список литературы

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


Рецензия

Для цитирования:


Кузьмин Е.В., Соколов В.А., Рябухин Д.А. Построение и верификация LD-программ ПЛК по LTL-спецификации. Моделирование и анализ информационных систем. 2013;20(6):78-94. https://doi.org/10.18255/1818-1015-2013-6-78-94

For citation:


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;20(6):78-94. (In Russ.) https://doi.org/10.18255/1818-1015-2013-6-78-94

Просмотров: 1114


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)