|
ИСТИНА |
Войти в систему Регистрация |
ИПМех РАН |
||
On some properties of timed finite state machinesстатья
- Авторы: Vinarskii E.M., Zakharov V.A.
- Журнал: Системная информатика
- Том: 17
- Год издания: 2020
- Первая страница: 11
- Последняя страница: 20
- Аннотация: Sequential reactive systems are formal models of programs that interact with the environment by receiving inputs and producing corresponding outputs. Such formal modelsare widely used in software engineering, computational linguistics, telecommunication, etc.In real life, the behavior of a reactive system depends not only on the flow of input data,but also on the time the input data arrive and the delays that occur when generatingresponses. To capture these aspects, a timed finite state machine (TFSM) is used as aformal model of a real-time sequential reactive system. However, in most of previouslyknown works, this model was considered in simplied semantics: transduction relations ofTFSMs are dened in such a way that the responses in the output stream, regardless oftheir timestamps, follow in the same order in which the corresponding inputs are deliveredto the machine. This simplication makes the model easier to analyze and manipulate, butit misses many important aspects of real-time computation. In this paper we study a morerealistic semantics of TFSMs and show how to represent it by means of Labeled TransitionSystems. This opens up a possibility to apply traditional formal methods for verifyingmore subtle properties of real-time reactive behavior which were previously ignored.
- Добавил в систему: Захаров Владимир Анатольевич