intechnguВестник НГУ. Серия: Информационные технологииVestnik NSU. Series: Information Technologies1818-79002410-0420НГУ10.25205/1818-7900-2018-16-4-85-94intechngu-64Research ArticleСтатьиАВТОМАТИЗИРОВАННАЯ ВЕРИФИКАЦИЯ АЛГОРИТМОВ УПРАВЛЕНИЯ СЛОЖНЫМИ ТЕХНОЛОГИЧЕСКИМИ ОБЪЕКТАМИ НА ПРОГРАММНЫХ ИМИТАТОРАХAUTOMATIC VERIFICATION OF CONTROL ALGORITHMS FOR COMPLEX TECHNOLOGICAL OBJECTS ON SOFTWARE SIMULATORSЛяхТ. В.LiakhT. V.antsys_nsu@mail.ruЗюбинВ. Е.ZyubinV. E.zyubin@iae.nsk.suГаранинаН. О.GaraninaN. O.garanina@iis.nsk.suИнститут автоматики и электрометрии СО РАНРоссияInstitute of Automation and Electrometry SB RASRussian FederationИнститут систем информатики им. А. П. Ершова СО РАНРоссияA. P. Ershov Institute of Informatics Systems SB RASRussian Federation2018301020201648594Copyright © Лях Т.В., Зюбин В.Е., Гаранина Н.О., 20202020Лях Т.В., Зюбин В.Е., Гаранина Н.О.Liakh T.V., Zyubin V.E., Garanina N.O.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://intechngu.elpub.ru/jour/article/view/64

Статья посвящена проблеме проверки алгоритмов управления, созданных в рамках процесс-ориентированного подхода, на соответствие входным спецификациям. Представлена общая схема верификации алгоритма управления, приведены ее реализация в автоматизированном варианте и результаты практической апробации в проекте по автоматизации Большого солнечного вакуумного телескопа.

The article is devoted to the analysis of process-oriented control algorithms, on the correspondence to input specifications. Article presents the general scheme of verification of the control algorithm, its implementation in an automated form and the results of practical approbation of the approach in the project for the automation of the Large Solar Vacuum Telescope.

автоматизацияпромышленные алгоритмы управленияверификацияпроцесс-ориентированные языки программированияautomationindustrial control algorithmsverificationprocess-oriented programming languagesReferencesЗакревский А. Д. Параллельные алгоритмы логического управления. М.: Эдиториал УРСС, 2003. 200 с.Закревский А. Д. Параллельные алгоритмы логического управления. М.: Эдиториал УРСС, 2003. 200 с.Wagner F., Schmuki R., Wagner T., Wolstenholme P. Modeling software with finite state machines: a practical approach // Auerbach Publications. 2006. 390 p.Wagner F., Schmuki R., Wagner T., Wolstenholme P. Modeling software with finite state machines: a practical approach // Auerbach Publications. 2006. 390 p.Harel D. Statecharts: A visual formalism for complex systems // Science of computer programming. 1987. Vol. 8.3. P. 231-274.Harel D. Statecharts: A visual formalism for complex systems // Science of computer programming. 1987. Vol. 8.3. P. 231-274.Зюбин В. Е. Программирование ПЛК: языки МЭК 61131-3 и возможные альтернативы // Промышленные АСУ и контроллеры. 2005. № 11. С. 31-35.Зюбин В. Е. Программирование ПЛК: языки МЭК 61131-3 и возможные альтернативы // Промышленные АСУ и контроллеры. 2005. № 11. С. 31-35.Лях Т. В., Зюбин В. Е., Сизов М. М. Опыт применения языка Reflex при автоматизации Большого солнечного вакуумного телескопа // Промышленные АСУ и контроллеры. 2016. № 7. С. 37-43.Лях Т. В., Зюбин В. Е., Сизов М. М. Опыт применения языка Reflex при автоматизации Большого солнечного вакуумного телескопа // Промышленные АСУ и контроллеры. 2016. № 7. С. 37-43.Зюбин В. Е. К пятилетию стандарта IEC 1131-3. Итоги и прогнозы // Приборы и системы. Управление, контроль, диагностика. 1999. № 1. C. 64-71.Зюбин В. Е. К пятилетию стандарта IEC 1131-3. Итоги и прогнозы // Приборы и системы. Управление, контроль, диагностика. 1999. № 1. C. 64-71.Samek M., Montgomery P. State Oriented Programming // Embedded Systems Programming. 2000. August. P. 22-43.Samek M., Montgomery P. State Oriented Programming // Embedded Systems Programming. 2000. August. P. 22-43.Шалыто А. А., Туккель Н. И. SWITCH технология - автоматный подход к созданию программного обеспечения «реактивных» систем // Программирование. 2001. № 5. С. 45-62.Шалыто А. А., Туккель Н. И. SWITCH технология - автоматный подход к созданию программного обеспечения «реактивных» систем // Программирование. 2001. № 5. С. 45-62.Розов А. С., Зюбин В. Е., Нефедов Д. В. Программирование встраиваемых микроконтроллерных систем на основе гиперпроцессов // Вестн. НГУ. Серия: Информационные технологии. 2017. Т. 15, № 4. С. 64-73.Розов А. С., Зюбин В. Е., Нефедов Д. В. Программирование встраиваемых микроконтроллерных систем на основе гиперпроцессов // Вестн. НГУ. Серия: Информационные технологии. 2017. Т. 15, № 4. С. 64-73.Зюбин В. Е. «Си с процессами» - язык программирования логических контроллеров // Мехатроника, автоматизация, управление. 2006. № 12. С. 31-35.Зюбин В. Е. «Си с процессами» - язык программирования логических контроллеров // Мехатроника, автоматизация, управление. 2006. № 12. С. 31-35.Зюбин В. Е. Итерационная разработка управляющих алгоритмов на основе имитационного моделирования объекта управления // Автоматизация в промышленности. 2010. № 11. С. 43-48.Зюбин В. Е. Итерационная разработка управляющих алгоритмов на основе имитационного моделирования объекта управления // Автоматизация в промышленности. 2010. № 11. С. 43-48.Розов А. С., Лях Т. В., Краснов Д. В., Санжиев Е. С. Практическая апробация языка IndustrialC на примере автоматизации установки термовакуумного напыления // Вестн. НГУ. Серия: Информационные технологии. 2017. Т. 15, № 3. С. 90-99.Розов А. С., Лях Т. В., Краснов Д. В., Санжиев Е. С. Практическая апробация языка IndustrialC на примере автоматизации установки термовакуумного напыления // Вестн. НГУ. Серия: Информационные технологии. 2017. Т. 15, № 3. С. 90-99.Гаранина Н. О., Зюбин В. Е., Лях Т. В. Онтологический подход к организации шаблонов требований в рамках системы поддержки формальной верификации программных систем. // Системная информатика. 2017. № 9. С. 111-132.Гаранина Н. О., Зюбин В. Е., Лях Т. В. Онтологический подход к организации шаблонов требований в рамках системы поддержки формальной верификации программных систем. // Системная информатика. 2017. № 9. С. 111-132.Shilov N. V., Garanina N. O. Combined Logics of Knowledge, Time, and Actions for Reasoning about Multi-agent Systems. Knowledge Processing and Data Analysis // Lecture Notes in Computer Science. 2011. Iss. 6581. P. 48-58.Shilov N. V., Garanina N. O. Combined Logics of Knowledge, Time, and Actions for Reasoning about Multi-agent Systems. Knowledge Processing and Data Analysis // Lecture Notes in Computer Science. 2011. Iss. 6581. P. 48-58.Шелехов В. И. Верификация и синтез программ сложения на базе правил корректности операторов // Моделирование и анализ информационных систем. 2010. Т. 17, № 4. С. 101-110.Шелехов В. И. Верификация и синтез программ сложения на базе правил корректности операторов // Моделирование и анализ информационных систем. 2010. Т. 17, № 4. С. 101-110.Clarke E. M., Gao S. Model checking hybrid systems // International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Lecture Notes in Computer Science. 2014. Iss. 8803. Р. 385-386.Clarke E. M., Gao S. Model checking hybrid systems // International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Lecture Notes in Computer Science. 2014. Iss. 8803. Р. 385-386.Clarke E. M., Grumberg O., Peled D. Model checking. MIT Press, 1999. 314 p.Clarke E. M., Grumberg O., Peled D. Model checking. MIT Press, 1999. 314 p.Clarke E. M., Emerson A., Sistla P. Automatic verification of finite-state concurrent systems using temporal logic specifications // ACM Transactions on Programming Languages and Systems. Vol. 8. Iss. 2. 1986. P. 244-263.Clarke E. M., Emerson A., Sistla P. Automatic verification of finite-state concurrent systems using temporal logic specifications // ACM Transactions on Programming Languages and Systems. Vol. 8. Iss. 2. 1986. P. 244-263.Isermann R., Schaffnit J., Sinsel S. Hardware-in-the-loop simulation for the design and testing of engine-control systems // Control Engineering Practice. 1999. Vol. 7. P. 643-653.Isermann R., Schaffnit J., Sinsel S. Hardware-in-the-loop simulation for the design and testing of engine-control systems // Control Engineering Practice. 1999. Vol. 7. P. 643-653.Xiao B., Starke M., King D., Irminger Ph., Herron A., Ollis B., Xue Y. Implementation of system level control and communications in a Hardware-in-the-Loop microgrid testbed // IEEE Power & Energy Society Innovative Smart Grid Technologies Conference (ISGT). 2016. P. 1-5.Xiao B., Starke M., King D., Irminger Ph., Herron A., Ollis B., Xue Y. Implementation of system level control and communications in a Hardware-in-the-Loop microgrid testbed // IEEE Power & Energy Society Innovative Smart Grid Technologies Conference (ISGT). 2016. P. 1-5.Зюбин В. Е. Использование виртуальных объектов для обучения программированию информационно-управляющих систем // Информационные технологии. 2009. № 6. С. 79-82.Зюбин В. Е. Использование виртуальных объектов для обучения программированию информационно-управляющих систем // Информационные технологии. 2009. № 6. С. 79-82.Лях Т. В., Зюбин В. Е. Автоматическая верификация алгоритмов управления сложными технологическими объектами на программных имитаторах // Математическое и компьютерное моделирование: Сб. материалов V Междунар. науч. конф., посвящ. памяти Р. Л. Долганова. Омск, 2017. С. 128-130.Лях Т. В., Зюбин В. Е. Автоматическая верификация алгоритмов управления сложными технологическими объектами на программных имитаторах // Математическое и компьютерное моделирование: Сб. материалов V Междунар. науч. конф., посвящ. памяти Р. Л. Долганова. Омск, 2017. С. 128-130.Зюбин В. Е., Калугин А. А. Виртуальные лабораторные стенды: обучение программированию задач промышленной автоматизации // Промышленные АСУ и контроллеры. 2009. № 2. С. 39-44.Зюбин В. Е., Калугин А. А. Виртуальные лабораторные стенды: обучение программированию задач промышленной автоматизации // Промышленные АСУ и контроллеры. 2009. № 2. С. 39-44.Ковадло П. Г., Лубков А. А., Бевзов А. Н., Будников К. И., Власов С. В., Зотов А. А., Колобов Д. Ю., Курочкин А. В., Котов В. Н., Лылов С. А., Лях Т. В., Максимов А. С., Перебейнос С. В., Петухов А. Д., Пещеров В. С., Попов Ю. А., Русских И. В., Томин В. Е. Система автоматизации Большого солнечного вакуумного телескопа // Автометрия. 2016. Т. 52, вып. 2. С. 97-106.Ковадло П. Г., Лубков А. А., Бевзов А. Н., Будников К. И., Власов С. В., Зотов А. А., Колобов Д. Ю., Курочкин А. В., Котов В. Н., Лылов С. А., Лях Т. В., Максимов А. С., Перебейнос С. В., Петухов А. Д., Пещеров В. С., Попов Ю. А., Русских И. В., Томин В. Е. Система автоматизации Большого солнечного вакуумного телескопа // Автометрия. 2016. Т. 52, вып. 2. С. 97-106.

The authors declare that there are no conflicts of interest present.