Рассуждения о программируемых логических контроллерах

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