Подход к автоматизации дедуктивной верификации процесс-ориентированных программ, основанный на шаблонах

Подход к автоматизации дедуктивной верификации процесс-ориентированных программ, основанный на шаблонах

Язык статьи
Английский
Аннотация
Процесс-ориентированное программирование — это подход к разработке управляющего программного обеспечения, в котором программа определяется как набор взаимодействующих процессов. PoST — это процесс-ориентированный язык, который является расширением язык ST из стандарта IEC 61131-3. В области разработки управляющего программного обеспечения формальная верификация играет важную роль вследствие необходимости обеспечения высокой надежности такого программного обеспечения. Дедуктивная верификация — это метод формальной верификации, в котором программа и требования к ней представляются в виде логических формул, а для доказательства того, что программа удовлетворяет требованиям, используется логический вывод. К управляющему программному обеспечению часто предъявляются темпоральные требования. Мы формализуем такие требования для процесс-ориентированных программ в виде инвариантов цикла управления. Но инварианты цикла управления, представляющие требования, недостаточны для доказательства корректности программы. Поэтому мы добавляем дополнительные инварианты, которые содержат вспомогательную информацию. В данной статье рассматривается проблема автоматизации дедуктивной верификации процесс-ориентированных программ. Мы предлагаем подход, в котором временные требования задаются с использованием шаблонов требований, которые строятся из базовых шаблонов. Для каждого шаблона требований определяются соответствующий шаблон дополнительных инвариантов и леммы. Предлагаемый подход позволяет сделать дедуктивную верификацию процесс-ориентированных программ более автоматизированной.
DOI
10.31144/si.2307-6410.2024.n25.p11-28
УДК
Страницы
11-28
Файл
Номер