|
Theory of computing
Темпоральная логика для программируемых логических контроллеров
Н. О. Гаранинаa, И. С. Ануреевa, В. Е. Зюбинb, С. М. Старолетовc, Т. В. Ляхb, А. С. Розовb, С. П. Горлачd a Институт систем информатики имени А.П. Ершова СО РАН, пр. Лаврентьева, д. 6, г. Новосибирск, 630090 Россия
b Институт автоматики и электрометрии СО РАН, пр. Акад. Коптюга, д. 1, г. Новосибирск, 630090 Россия
c Алтайский государственный технический университет им. И.И. Ползунова, пр. Ленина, д. 46, г. Барнаул, 656038 Россия
d Университет Мюнстера, Шлосплац, д. 2, Мюнстер, 48149 Германия
Аннотация:
Мы исследуем формальную верификацию управляющего программного обеспечения критических систем, т. е. проверку соответствия функционирования проектируемой системы предъявленным требованиям. Важнейший класс управляющего программного обеспечения составляют программы для программируемых логических контроллеров (ПЛК). Особенностью программ ПЛК является цикл управления: 1) считываются входы, 2) изменяются состояния ПЛК и 3) записываются выходы. Поэтому для формальной верификации программ ПЛК нужна возможность описывать учитывающие эту специфику системы переходов, а также определять свойства систем, моделирующих программы ПЛК, как относительно переходов внутри цикла, так и относительно более крупных переходов в соответствии с семантикой цикла управления. Мы предлагаем формальную модель программы ПЛК как систему переходов гиперпроцессов и темпоральную логику cycle-LTL для формализации свойств ПЛК. Особенностью логики cycle-LTL является возможность рассматривать свойства систем управления двояким образом: воздействие окружения на систему управления и воздействие системы управления на окружение. Мы определяем модификации стандартных темпоральных операторов логики LTL для каждого из этих случаев, а также для свойств внутри цикла управления. Рассмотрены примеры требований, определенных в нашей логике. Описана трансляция формул cycle-LTL в формулы LTL и показана её корректность. Доказана возможность сведения задачи верификации методом проверки моделей для требований, определенных в логике cycle-LTL, к задаче верификации требований, определенных в стандартной логике LTL.
Ключевые слова:
формальная верификация, темпоральная логика, системы переходов, программируемые логические контроллеры (ПЛК).
Поступила в редакцию: 12.11.2020 Исправленный вариант: 12.12.2020 Принята в печать: 16.12.2020
Образец цитирования:
Н. О. Гаранина, И. С. Ануреев, В. Е. Зюбин, С. М. Старолетов, Т. В. Лях, А. С. Розов, С. П. Горлач, “Темпоральная логика для программируемых логических контроллеров”, Модел. и анализ информ. систем, 27:4 (2020), 412–427
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/mais725 https://www.mathnet.ru/rus/mais/v27/i4/p412
|
Статистика просмотров: |
Страница аннотации: | 72 | PDF полного текста: | 43 | Список литературы: | 11 |
|