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

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