On the Modeling of Sequential Reactive Systems by Means of Real Time Automata
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 con...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2020-12-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/1432 |
| _version_ | 1797877830159171584 |
|---|---|
| author | Evgeney Maximovich Vinarskii Vladimir Anatolyevich Zakharov |
| author_facet | Evgeney Maximovich Vinarskii Vladimir Anatolyevich Zakharov |
| author_sort | Evgeney Maximovich Vinarskii |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-10T02:24:18Z |
| format | Article |
| id | doaj.art-c42fc8cd23f7451294a5e81947f16176 |
| institution | Directory Open Access Journal |
| issn | 1818-1015 2313-5417 |
| language | English |
| last_indexed | 2024-04-10T02:24:18Z |
| publishDate | 2020-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj.art-c42fc8cd23f7451294a5e81947f161762023-03-13T08:07:35ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172020-12-0127439641110.18255/1818-1015-2020-4-396-4111088On the Modeling of Sequential Reactive Systems by Means of Real Time AutomataEvgeney Maximovich Vinarskii0Vladimir Anatolyevich Zakharov1Московский государственный университет имени М.В. ЛомоносоваМосковский государственный университет имени М.В. Ломоносова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.https://www.mais-journal.ru/jour/article/view/1432реагирующая системаконечный автоматверификациясвойство безопасностиразмеченная система переходовсимуляция |
| spellingShingle | Evgeney Maximovich Vinarskii Vladimir Anatolyevich Zakharov On the Modeling of Sequential Reactive Systems by Means of Real Time Automata Моделирование и анализ информационных систем реагирующая система конечный автомат верификация свойство безопасности размеченная система переходов симуляция |
| title | On the Modeling of Sequential Reactive Systems by Means of Real Time Automata |
| title_full | On the Modeling of Sequential Reactive Systems by Means of Real Time Automata |
| title_fullStr | On the Modeling of Sequential Reactive Systems by Means of Real Time Automata |
| title_full_unstemmed | On the Modeling of Sequential Reactive Systems by Means of Real Time Automata |
| title_short | On the Modeling of Sequential Reactive Systems by Means of Real Time Automata |
| title_sort | on the modeling of sequential reactive systems by means of real time automata |
| topic | реагирующая система конечный автомат верификация свойство безопасности размеченная система переходов симуляция |
| url | https://www.mais-journal.ru/jour/article/view/1432 |
| work_keys_str_mv | AT evgeneymaximovichvinarskii onthemodelingofsequentialreactivesystemsbymeansofrealtimeautomata AT vladimiranatolyevichzakharov onthemodelingofsequentialreactivesystemsbymeansofrealtimeautomata |