О моделировании последовательных реагирующих систем при помощи автоматов, работающих в реальном времени

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