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

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

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

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

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