Процесс-ориентированное программирование — это подход к разработке управляющего программного обеспечения, в котором программа определяется как набор взаимодействующих процессов. PoST — это процесс-ориентированный язык, который является расширением языка ST из стандарта IEC 61131-3. В области разработки управляющего программного обеспечения формальная верификация играет важную роль вследствие необходимости обеспечения высокой надежности такого программного обеспечения. Дедуктивная верификация — это метод формальной верификации, в котором программа и требования к ней представляются в виде логических формул, а для доказательства того, что программа удовлетворяет требованиям, используется логический вывод. К управляющему программному обеспечению часто предъявляются темпоральные требования. Мы формализуем такие требования для процесс-ориентированных программ в виде инвариантов цикла управления. Но инварианты цикла управления, представляющие требования, недостаточны для доказательства корректности программы. Поэтому мы добавляем дополнительные инварианты, которые содержат вспомогательную информацию. В данной статье рассматривается проблема автоматизации дедуктивной верификации процесс-ориентированных программ. Предложен подход, в котором темпоральные требования задаются с использованием шаблонов требований, которые строятся из базовых шаблонов. Для каждого шаблона требований определяются соответствующий шаблон дополнительных инвариантов и леммы. В статье описан предлагаемый подход и схемы базовых и производных шаблонов требований. Рассмотрены схемы базовых шаблонов дополнительных инвариантов, схемы лемм, определяемых для базовых шаблонов, а также набор базовых шаблонов и леммы для них. Определены схема производных шаблонов дополнительных инвариантов и схемы лемм, определяемых для производных шаблонов. Представлены алгоритмы построения производных шаблонов дополнительных инвариантов и лемм для них, а также метод доказательства этих лемм. Рассмотрены схемы доказательства условий корректности. Предложенный подход демонстрируется на примере. Также проведен анализ связанных работ.
Классическая дедуктивная верификация не ориентирована на доказательство некорректности программ. Доказательство некорректности программ с помощью формальных методов является актуальной задачей в настоящее время. Специальные логики, такие как Incorrectness Logic, Adversarial Logic, Local Completeness Logic, Exact Separation Logic и Outcome Logic, были недавно предложены для решения данной задачи. Но у данных логик имеется два недостатка. Во-первых, в данных логиках используются подходы, основанные на нижней аппроксимации, тогда как в классической дедуктивной верификации используется подход, основанный на верхней аппроксимации. С другой стороны, использование классического подхода требует в общем случае задания инвариантов циклов. Во-вторых, использование правил вывода для программных конструкций в их самом общем виде приводит к необходимости доказательства сложных формул в простых ситуациях. Нашим результатом, представленным в данной статье, является новая логика для решения данных проблем в случае циклов над последовательностями данных. Такая циклы мы называем финитными итерациями. Предложенную логику мы называем логикой для суждений о некорректности финитных итераций (IFIL). Мы избегаем задания инвариантов финитных итераций с помощью символической замены в условиях корректности переменных таких циклов применениями рекурсивных функций. Наша логика основана на специальных правилах вывода для финитных итераций. Эти правила позволяют выводить формулы с применениями рекурсивных функций, соответствующих финитным итерациям. Истинность этих формул может означать наличие ошибок в финитных итерациях. Данная логика была реализована в новой версии программной системы C“=lightVer для дедуктивной верификации программ на языке C.