Шаблоны требований в дедуктивной верификации poST-программ

Процесс-ориентированное программирование — один из подходов к разработке управляющего программного обеспечения. Процесс-ориентированная программа определяется как последовательность процессов. Каждый процесс представляется набором именованных состояний, содержащих программный код, которые задают логику поведения процесса. Выполнение программы заключается в последовательном исполнении этих процессов в их текущих состояниях на каждой итерации цикла управления. Процессы могут взаимодействовать через изменение состояний друг друга и через разделяемые переменные.
Статья является развитием метода классификации темпоральных требований к процесс-ориентированным программам с целью упростить и автоматизировать дедуктивную верификацию таких программ. Метод состоит из следующих шагов. На первом шаге требования формализуются на специализированном языке DV-TRL, варианте типизированной логики предикатов первого порядка с набором интерпретированных типов и предикатных и функциональных символов, позволяющем отражать специфические понятия систем управления в процесс-ориентированной парадигме. На втором шаге формализованные требования разбиваются на классы, каждый из которых определяется шаблоном — параметрической формулой языка DV-TRL, причем условия корректности, порождаемые для процесс-ориентированных программ относительно требований, удовлетворяющих одному шаблону, имеют одну и ту же схему доказательства. На третьем шаге разрабатываются соответствующие схемы доказательства. В статье мы сначала даём краткое введение в язык poST, процесс-ориентированное расширение языка ST стандарта МЭК 61131-3. Далее определяется язык DV-TRL. Мы также приводим коллекцию требований на естественном языке для нескольких систем управления. Затем мы определяем шаблоны, позволяющие полностью покрыть все требования этой коллекции и для каждого из шаблонов приводим пример формализованного требования из коллекции и описываем схему доказательства условий корректности для этого шаблона. Статистика распределения требований из коллекции по шаблонам выявляет наиболее востребованные шаблоны. Мы также провели анализ связанных работ.