On the Modeling of Sequential Reactive Systems by Means of Real Time Automata

Automatic Control and Computer Sciences. 2021. Vol. 55. No. 7. P. 751–762.

Vinarskii E., Zakharov V.

Translator: Zakharov V.

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 input sequences, but also by their timestamps 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, real-time 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 of their timestamps, follow in the same order as the corresponding
elements of the 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 for the solution of verification
problems in the framework of this model. For this purpose, we suggest an alternative definition of
TFSM computations by means of labeled transition systems and show that the both 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 of sequential reactive systems.

Keywords: simulation, transition systems, reactive system, реагирующая система, formal verification, конечный автомат реального времени, формальная верификация модели, Finite State Machine (FSM), размеченная система переходов, отношение симуляции

Publication based on the results of: Process models: checking conformance with the observed behavior, automated discovery and behavioral analysis (2021)