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

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

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

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