Доктор физико-математических наук, профессор
Doctor of sciences, professor
Последовательные реагирующие системы включают в себя устройства и программы, вычисления которых состоят в непрерывном взаимодействии с внешней средой, от которой они получают потоки входных сигналов (данных, команд) и в ответ на них формируют потоки выходных сигналов. К системам такого вида относятся контроллеры, сетевые коммутаторы, интерпретаторы программ, системные драйверы. Поведение некоторых реагирующих систем определяется не только последовательностью значений входных сигналов, но также временем их поступления на вход системы и задержками вычисления выходных сигналов. Эти особенности вычисления реагирующих систем хорошо учитываются вычислительными моделями реального времени, к числу которых относятся, в частности, конечные автоматы-преобразователи реального времени (Timed Finite State Machines, TFSMs). Однако в большинстве работ, посвященных изучению этой модели вычислений, используется упрощенная семантика TFSMs: элементы выходного потока, независимо от сопутствующих пометок времени, располагаются в том же порядке, в котором следуют соответствующие им элементы входного потока. Такое упрощение семантики делает модель менее адекватной для многих приложений, но зато облегчает решение задач анализа и преобразования таких автоматов. В данной статье мы изучаем модель TFSM с более реалистичной семантикой. Переход к новой модели TFSM требует и новых подходов к решению задачи верификации автоматов в этой модели. Для этой цели мы предлагаем альтернативное определение вычислений TFSM с использованием размеченных систем переходов и показываем, что два определения семантики для рассматриваемого класса автоматов реального времени хорошо взаимосвязаны друг с другом. Использование семантики TFSM, основанной на размеченных системах переходов, открывает возможность применения ранее известных методов верификации систем вычислений реального времени для анализа поведения последовательных реагирующих систем.
Sequential reactive systems include hardware devices and software programs which operate in continuous interaction with the external environment, from which they receive streams of input signals (data, commands) and in response to them form streams of output signals. Systems of this type include controllers, network switches, program interpreters, system drivers. The behavior of some reactive systems is determined not only by the sequence of values of input signals, but also by the time of their arrival at the inputs of the system and the delays in computing the output signals. These aspects of reactive system computations are taken into account by real-time models of computation which include, in particular, realtime finite state machines (TFSMs). However, in most works where this class of real-time automata is studied a simple variant of TFSM semantics is used: the transduction relation computed by a TFSM is defined so that the elements of an output stream, regardless oftheir timestamps, follow in the same order as the corresponding elements ofthe input stream. This straightforward approach makes the model easier to analyze and manipulate, but it misses many important features of real-time computation. In this paper we study a more realistic semantics of TFSMs and show how to represent it by means of Labeled Transition Systems. The use of the new TFSM model also requires new approaches to the solution of verification problems in the framework of this model. For this purpose, we propose an alternative definition of TFSM computations by means of Labeled Transition Systems and show that the two definitions of semantics for the considered class of real-time finite state machines are in good agreement with each other. The use of TFSM semantics based on Labeled Transition Systems opens up the possibility of adapting well known real-time model checking techniques to the verification ofsequential reactive systems.
The authors declare that there are no conflicts of interest present.