Темпоральная логика для программируемых логических контроллеров

Мы исследуем формальную верификацию управляющего программного обеспечения критических систем, т. е. проверку соответствия функционирования проектируемой системы предъявленным требованиям. Важнейший класс управляющего программного обеспечения составляют программы для программируемых логических контроллеров (ПЛК). Особенностью программ ПЛК является цикл управления: 1) считываются входы, 2) изменяются состояния ПЛК и 3) записываются выходы. Поэтому для формальной верификации программ ПЛК нужна возможность описывать учитывающие эту специфику системы переходов, а также определять свойства систем, моделирующих программы ПЛК, как относительно переходов внутри цикла, так и относительно более крупных переходов в соответствии с семантикой цикла управления. Мы предлагаем формальную модель программы ПЛК как систему переходов гиперпроцессов и темпоральную логику cycle-LTL для формализации свойств ПЛК. Особенностью логики cycle-LTL является возможность рассматривать свойства систем управления двояким образом: воздействие окружения на систему управления и воздействие системы управления на окружение. Мы определяем модификации стандартных темпоральных операторов логики LTL для каждого из этих случаев, а также для свойств внутри цикла управления. Рассмотрены примеры требований, определенных в нашей логике. Описана трансляция формул cycle-LTL в формулы LTL и показана её корректность. Доказана возможность сведения задачи верификации методом проверки моделей для требований, определенных в логике cycle-LTL, к задаче верификации требований, определенных в стандартной логике LTL.