Системная информатика, 2020, № 17

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

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

Последовательные реагирующие системы, такие как контроллеры, системные драйверы, компьютерные интерпретаторы, работают с двумя потоками данных и преобразуют входные потоки данных (управляющие сигналы, инструкции) в выходные потоки управляющих сигналов (инструкции, данные). Конечные преобразователи широко используются в качестве подходящей формальной модели для подобных систем обработки информации. Поскольку вычисления преобразователей протекают во времени, темпоральная логика, очевидно, может использоваться как простой и выразительный формализм для определения поведения последовательных реагирующих систем. Однако обычные прикладные темпоральные логики (LTL, CTL) плохо подходят для этой цели, поскольку их формулы интерпретируются на омега-языках, тогда как поведение преобразователей представлено бинарными отношениями на бесконечных последовательностях, то есть омега-трансдукциях. Чтобы обеспечить темпоральную логику возможностью учитывать эту общую особенность поведения реагирующих систем, мы ввели новые расширения этой логики. Это расширение характеризуют две отличительные особенности: 1) временные операторы параметризуются наборами потоков (языков), допустимых для ввода, и 2) наборы (языки) ожидаемых выходных потоков используются в качестве базовых предикатов. В предыдущей серии работ мы изучали выразительные возможности и задачу верификации моделей для Reg-LTL и Reg-CTL, которые являются такими расширениями LTL и CTL, где упомянутые выше языки являются регулярными. Мы обнаружили, что такое расширение темпоральной логики увеличивает их выразительную способность, хотя сохраняет разрешимость задачи верификации моделей. Нашим следующим шагом в систематическом изучении выразительных и алгоритмических свойств новых расширений темпоральной логики является анализ проблемы верификации моделей для конечных автоматов-преобразователей относительно формул логики Reg-CTL*. В этой статье мы описываем алгоритм верификации моделей автоматов-преобразователей для форму логики Reg-CTL* и показываем, что эта задача принадлежит классу сложности ExpSpace.

Мы рассматриваем формальную проверку программного обеспечения управления критическими системами, то есть обеспечение отсутствия ошибок проектирования в системе по отношению к требованиям. Системы управления обычно основаны на промышленных контроллерах, также известных как программируемые логические контроллеры (ПЛК). Специфической особенностью ПЛК является цикл сканирования: 1) считываются входы, 2) изменяются состояния ПЛК и 3) записываются выходы. Поэтому для формальной верификации ПЛК, например, путем проверки модели, необходимо рассуждать как в терминах переходов состояний внутри цикла, так и в терминах более крупных переходов состояний в соответствии с семантикой циклов.
Мы разрабатываем формализацию ПЛК как гиперпроцессной системы переходов и основанный на LTL временной логике cycle-LTL для рассуждений о ПЛК.

Описывается дедуктивная верификация программы kstrtoul на языке Си из библиотеки ОС Linux. Программа kstrtoul реализует вычисление целого числа, представленного в виде последовательности литер. Чтобы упростить верификацию, применяются трансформации замены операций с указателями эквивалентными действиями без указателей. Программа преобразуется на язык предикатного программирования. Конструируется модель внутреннего состояния программы как часть спецификации программы. Дедуктивная верификация проведена в системах Why3 и Coq.