Моделирование согласованного поведения ПЛК-датчиков


https://doi.org/10.18255/1818-1015-2014-4-75-90

Полный текст:


Аннотация

Статья продолжает цикл работ, посвященный разработке подхода к построению и верификации «дискретных» программ логических контроллеров (ПЛК), обеспечивающего возможность анализа их корректности с помощью метода проверки модели (model checking). Подход получил название «Программирование и верификация по LTL-спецификации». При верификации ПЛК-программы методом проверки модели возникает необходимость в построении ее конечной модели.

При этом для успешной проверки соответствия модели требуемым программным свойствам важно учитывать то, что далеко не все комбинации входных сигналов от датчиков могут встречаться в действительности при работе ПЛК с объектом управления. Этот факт требует более внимательного отношения к построению модели программы ПЛК.

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

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


Об авторах

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


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


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


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

1. Рябухин Д. А., Кузьмин Е. В., Соколов В. А. Построение IL-программ ПЛК по LTL-спецификации // Моделирование и анализ информационных систем. 2014. Т. 21, №2. С. 26–38. (Ryabukhin D. A., Kuzmin E. V., Sokolov V. A. Construction of PLC IL-programs by LTLspecification // Modeling and analysis of information systems. 2014. V. 21, №2. P. 26–38 [in Russian]).

2. Кузьмин Е. В., Соколов В. А., Рябухин Д. А. Построение и верификация LD-программ ПЛК по LTL-спецификации // Моделирование и анализ информационных систем. 2013. Т. 20, №6. С. 78–94. (Kuzmin E. V., Sokolov V. A., Ryabukhin D. A. Construction and Verification of PLC LDprograms by LTL-specification // Modeling and analysis of information systems. 2013. V. 20, №6. P. 78–94 [in Russian]).

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

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

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

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


Дополнительные файлы

Для цитирования: Кузьмин Е.В., Рябухин Д.А., Соколов В.А. Моделирование согласованного поведения ПЛК-датчиков. Моделирование и анализ информационных систем. 2014;21(4):75-90. https://doi.org/10.18255/1818-1015-2014-4-75-90

For citation: Kuzmin E.V., Ryabukhin D.A., Sokolov V.A. Modeling a Consistent Behavior of PLC-Sensors. Modeling and Analysis of Information Systems. 2014;21(4):75-90. (In Russ.) https://doi.org/10.18255/1818-1015-2014-4-75-90

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

Обратные ссылки

  • Обратные ссылки не определены.


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


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