Системная информатика, 2024, № 25

Системы управления играют решающую роль в различных областях, требующих высокой надежности и подтверждения правильности работы программного обеспечения. Для решения этой проблемы используются формальные методы, такие как дедуктивная верификация, которые математически обеспечивают корректность программного обеспечения, критически важного для безопасности. Этот процесс включает в себя генерацию условий корректности на основе аксиоматической семантики программы и ее требований. Основным недостатком ручной генерации условий корректности является ее трудоемкость и подверженность человеческим ошибкам, что приводит к разработке автоматизированных генераторов условий проверки. Однако они создают избыточные или чрезмерно сложные условия проверки, которые неточно отражают возможные пути работы программы. Для устранения второй проблемы были введены предметно-ориентированные языки, такие как Reflex, которые используют процесс-ориентированную парадигму для оптимизации программирования и упрощения генерации условий проверки. Тем не менее, присущая Reflex структура switch-case может привести к увеличению числа условий корректности, усугубляя первую проблему и усложняя выбор подходящих. В данной статье предлагается простая система статического анализа, предназначенная для оптимизации генерации условий корректности для программ Reflex, что повышает эффективность процесса верификации. Она основана на привязке атрибутов к различным операторам. Затем на протяжении всего процесса генерации условий корректности эти атрибуты собираются и проверяются на совместимость с ранее собранными. Если атрибуты несовместимы, то условия корректности отбрасываются.

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

В этой статье мы формально описываем системы реального времени с абстрактным планировщиком, используя модели Крипке. Эта формализация позволяет специализировать абстрактный планировщик в терминах построенной модели. Мы иллюстрируем этот подход с помощью системы реального времени, в которой работы являются невытесняемыми и имеют фиксированный приоритет (NE-GFP). Мы также формулируем свойство безопасности для систем реального времени, используя линейную временную логику LTL. Мы реализуем нашу формализацию систем реального времени с планировщиком NE-GFP на языке Promela, используемом в инструменте проверки SPIN, и проводим эксперименты для доказательства/опровержения свойства безопасности, чтобы оценить эффективность нашего подхода.

Вероятности достижимости и ожидаемые вознаграждения - это два важных класса свойств, которые используются при проверке вероятностной модели. Для вычисления базовых свойств применяются итерационные численные методы. Чтобы гарантировать достоверность результатов вычислений, используется метод интервальных итераций. Этот метод использует два вектора в качестве верхней и нижней границ значений и использует стандартный метод итерации значений для обновления значений этих векторов. В этой статье мы используем комбинацию итерации значений и итерации политики для обновления этих значений. Мы используем итерацию политики для обновления значений вектора с нижней границей. Для вектора с верхней границей мы используем модифицированную версию итерации значений, которая помечает бесполезные действия, чтобы игнорировать их в оставшейся части вычислений. Предлагаемый нами подход дает возможность применить некоторые передовые методы для сокращения времени выполнения вычислений для метода интервальных итераций. Мы рассматриваем набор стандартных примеров, и экспериментальные результаты показывают, что в большинстве случаев предлагаемый нами метод сокращает время выполнения вычислений.