On the Modeling of Sequential Reactive Systems by Means of Real Time Automataстатья
Информация о цитировании статьи получена из
Web of Science,
Scopus
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 4 марта 2022 г.
Аннотация:Sequential reactive systems include hardware devices and software programs which operatein continuous interaction with the external environment, from which they receive streams of input signals (data, commands) and in response to them form streams of by 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 sequence, 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.