Эта статья посвящена использованию метода верификации моделей для точного теста планируемости систем реального времени, выполняющихся на мультипроцессорных платформах. Чтобы использовать этот метод, мы формально описываем системы реального времени с абстрактным планировщиком, используя модели Крипке. Эта формализация содержит термины, достаточные для специализации абстрактного планировщика. Мы иллюстрируем наш подход, явно определяя планировщики, которые учитывают вытеснение/невытеснение задач и глобальный фиксированный приоритет или приоритет ближайшего дедлайна в различных сочетаниях. Свойство безопасности (планируемости) систем реального времени сформулировано с помощью линейной темпоральной логики LTL. Формализация систем реального времени как моделей Крипке и задание свойства безопасности (планируемости) как формулы LTL позволяет свести точный тест планируемости таких систем к задаче верификации моделей. Мы апробируем этот подход к точному тесту планируемости, реализуя на Promela — входном языке инструмента верификации моделей SPIN — нашу формализацию систем реального времени с невытесняющим планировщиком с глобальным фиксированным приоритетом (NP-GFP), вытесняющим планировщиком с глобальным фиксированным приоритетом (P-GFP), невытесняющим планировщиком с приоритетом ближайшего дедлайна (NP-EDF) и вытесняющим планировщиком с приоритетом ближайшего дедлайна (P-EDF). Мы проводим эксперименты в SPIN для доказательства/опровержения свойства безопасности (планируемости), чтобы оценить эффективность нашего подхода. Мы предлагаем эвристическую оценку планируемости системы реального времени на основе доказуемости небезопасности и недоказуемости безопасности системы реального времени при выполнении на мультипроцессорных платформах с числом процессоров, отличающимся на единицу.
В работе рассматривается класс расширенных регулярных выражений с обратными ссылками, которые представляются как элементы полукольца, частично удовлетворяющего теоремам алгебры Клини. Используя эти теоремы в качестве правил переписывания, возможно построить алгоритм устранения неоднозначности в ячейках памяти выражений. В дальнейшем этот алгоритм может быть применён для построения обращений расширенных регулярных выражений в заданных ограничениях. Предложенные алгоритмы были апробированы на тестовой выборке регулярных выражений, построенных на базе выражений из RegexLib и StackOverflow. Результаты экспериментов показали, что в ряде случае время сопоставления с преобразованным регулярным выражением было значительно меньше, чем с исходным.
Процесс-ориентированное программирование — это подход к разработке управляющего программного обеспечения, в котором программа определяется как набор взаимодействующих процессов. PoST — это процесс-ориентированный язык, который является расширением языка ST из стандарта IEC 61131-3. В области разработки управляющего программного обеспечения формальная верификация играет важную роль вследствие необходимости обеспечения высокой надежности такого программного обеспечения. Дедуктивная верификация — это метод формальной верификации, в котором программа и требования к ней представляются в виде логических формул, а для доказательства того, что программа удовлетворяет требованиям, используется логический вывод. К управляющему программному обеспечению часто предъявляются темпоральные требования. Мы формализуем такие требования для процесс-ориентированных программ в виде инвариантов цикла управления. Но инварианты цикла управления, представляющие требования, недостаточны для доказательства корректности программы. Поэтому мы добавляем дополнительные инварианты, которые содержат вспомогательную информацию. В данной статье рассматривается проблема автоматизации дедуктивной верификации процесс-ориентированных программ. Предложен подход, в котором темпоральные требования задаются с использованием шаблонов требований, которые строятся из базовых шаблонов. Для каждого шаблона требований определяются соответствующий шаблон дополнительных инвариантов и леммы. В статье описан предлагаемый подход и схемы базовых и производных шаблонов требований. Рассмотрены схемы базовых шаблонов дополнительных инвариантов, схемы лемм, определяемых для базовых шаблонов, а также набор базовых шаблонов и леммы для них. Определены схема производных шаблонов дополнительных инвариантов и схемы лемм, определяемых для производных шаблонов. Представлены алгоритмы построения производных шаблонов дополнительных инвариантов и лемм для них, а также метод доказательства этих лемм. Рассмотрены схемы доказательства условий корректности. Предложенный подход демонстрируется на примере. Также проведен анализ связанных работ.
Процесс-ориентированное программирование - один из подходов к разработке управляющего программного обеспечения. Процесс-ориентированная программа определяется как последовательность процессов. Каждый процесс представляется набором именованных состояний, содержащих программный код, которые задают логику поведения процесса. Выполнение программы заключается в последовательном исполнении этих процессов в их текущих состояниях на каждой итерации цикла управления. Процессы могут взаимодействовать через изменение состояний друг друга и через разделяемые переменные. Статья является развитием метода классификации темпоральных требований к процесс-ориентированным программам с целью упростить и автоматизировать дедуктивную верификацию таких программ. Метод состоит из следующих шагов. На первом шаге требования формализуются на специализированном языке DV-TRL, варианте типизированной логики предикатов первого порядка с набором интерпретированных типов и предикатных и функциональных символов, позволяющем отражать специфические понятия систем управления в процесс-ориентированной парадигме. На втором шаге формализованные требования разбиваются на классы, каждый из которых определяется шаблоном - параметрической формулой языка DV-TRL, причем условия корректности, порождаемые для процесс-ориентированных программ относительно требований, удовлетворяющих одному шаблону, имеют одну и ту же схему доказательства. На третьем шаге разрабатываются соответствующие схемы доказательства. В статье мы сначала даём краткое введение в язык poST, процесс-ориентированное расширение языка ST стандарта МЭК 61131-3. Далее определяется язык DV-TRL. Мы также приводим коллекцию требований на естественном языке для нескольких систем управления. Затем мы определяем шаблоны, позволяющие полностью покрыть все требования этой коллекции и для каждого из шаблонов приводим пример формализованного требования из коллекции и описываем схему доказательства условий корректности для этого шаблона. Статистика распределения требований из коллекции по шаблонам выявляет наиболее востребованные шаблоны. Мы также провели анализ связанных работ.