Preview

Моделирование и анализ информационных систем

Расширенный поиск

О моделировании последовательных реагирующих систем при помощи автоматов, работающих в реальном времени

https://doi.org/10.18255/1818-1015-2020-4-396-411

Полный текст:

Аннотация

Последовательные реагирующие системы включают в себя устройства и программы, вычисления которых состоят в непрерывном взаимодействии с внешней средой, от которой они получают потоки входных сигналов (данных, команд) и в ответ на них формируют потоки выходных сигналов. К системам такого вида относятся контроллеры, сетевые коммутаторы, интерпретаторы программ, системные драйверы. Поведение некоторых реагирующих систем определяется не только последовательностью значений входных сигналов, но также временем их поступления на вход системы и задержками вычисления выходных сигналов. Эти особенности вычисления реагирующих систем хорошо учитываются вычислительными моделями реального времени, к числу которых относятся, в частности, конечные автоматы-преобразователи реального времени (Timed Finite State Machines, TFSMs). Однако в большинстве работ, посвященных изучению этой модели вычислений, используется упрощенная семантика TFSMs: элементы выходного потока, независимо от сопутствующих пометок времени, располагаются в том же порядке, в котором следуют соответствующие им элементы входного потока. Такое упрощение семантики делает модель менее адекватной для многих приложений, но зато облегчает решение задач анализа и преобразования таких автоматов. В данной статье мы изучаем модель TFSM с более реалистичной семантикой. Переход к новой модели TFSM требует и новых подходов к решению задачи верификации автоматов в этой модели. Для этой цели мы предлагаем альтернативное определение вычислений TFSM с использованием размеченных систем переходов и показываем, что два определения семантики для рассматриваемого класса автоматов реального времени хорошо взаимосвязаны друг с другом. Использование семантики TFSM, основанной на размеченных системах переходов, открывает возможность применения ранее известных методов верификации систем вычислений реального времени для анализа поведения последовательных реагирующих систем.

Об авторах

Евгений Максимович Винарский
Московский государственный университет имени М.В. Ломоносова
Россия


Владимир Анатольевич Захаров
Московский государственный университет имени М.В. Ломоносова
Россия

Доктор физико-математических наук, профессор



Список литературы

1. A. Gill et al., «Introduction to the Theory of Finite-state Machines», 1962.

2. A. Y. Savelev, «Prikladnaya teoriya cifrovyh avtomatov», 1987, In Russian.

3. R. Alur and D. Dill, «A theory of timed automata», Theoretical computer science, vol. 126, no. 2, pp. 183-235, 1994.

4. E. Asarin, P. Caspi, and O. Maler, «Timed regular expressions», Journal of the ACM, vol. 49, no. 2, pp. 1-35, 2001.

5. E. Asarin, P. Caspi, and O. Maler, «A Kleene theorem for timed automata», in Proceedings of 12-th Annual IEEE Symposium on Logic in Computer Science (LICS'97), IEEE, 1997, pp. 160-171.

6. R. Alur and P. Madhusudan, «Decision Problems for Timed Automata: A Survey, Formal Methods for the Design of Real-Time Systems», in Proceedings of the 4-th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM'04), Springer, 2004, pp. 1-24.

7. S. Lasota and I. Walukiewicz, «Alternating timed automata», ACM Transactions on Computational Logic (TOCL), vol. 9, no. 2, pp. 1-26, 2008.

8. M. Gromov, K. El-Fakih, N. Shabaldina, and N. Yevtushenko, «Distinguing Non-deterministic Timed Finite State Machines», in Formal Techniques for Distributed Systems, Lecture Notes in Computer Science, vol. 5522, Springer, 2009, pp. 137-151.

9. M. G. Merayo, M. Nunez, and I. Rodriguez, «Formal testing from timed finite state machines», Computer networks, vol. 52, no. 2, pp. 432-460, 2008.

10. D. Bresolin, K. El-Fakih, T. Villa, and N. Yevtushenko, «Deterministic Timed Finite State Machines: Equivalence Checking and Expressive Power», Proceedings of the 5-th International Symposium on Games, Automata, Logics and Formal Verification, pp. 203-216, 2014.

11. A. Tvardovskii and N. Yevtushenko, «Minimizing timed Finite State Machines», Tomsk State University Journal of Controland Computer Science, vol. 29, no. 4, pp. 77-83, 2014.

12. A. S. Tvardovskii, N. V. Yevtushenko, and M. L. Gromov, «Minimizing finite state machines with time guards and timeouts», Proceedings of the Institute for System Programming of the RAS, vol. 29, no. 4, pp. 139-154, 2017.

13. A. S. Tvardovskii and N. V. Yevtushenko, «Deriving homing sequences for Finite State Machines with timed guards», Sistemnaya informatika, vol. 17, pp. 1-10, 2020.

14. N. McKeown, T. Anderson, H. Balakrishnan, G. Parulkar, L. Peterson, J. Rexford, S. Shenker, and J. Turner, «OpenFlow: enabling innovation in campus networks», ACM SIGCOMM Computer Communication Review, vol. 38, no. 2, pp. 69-74, 2008.

15. E. Vinarskii, J. Lopez, N. Kushik, N. Yevtushenko, and D. Zeghlache, «A Model Checking Based Approach for Detecting SDN Races», in Proceedings of the 31-st IFIP WG 6.1 International Conference on Testing Software and Systems (ICTSS), Springer, 2019, pp. 194-211.

16. E. M. Vinarskii and V. A. Zakharov, «On the verification of strictly deterministic behavior of Timed Finite State Machines», Proceedings of ISP RAS, vol. 30, no. 3, pp. 325-340, 2018.

17. C. Baier and J.-P. Katoen, Principles ofmodel checking. Cambridge: MIT Press Cambridge, 2008.

18. G. Behrmann, A. David, and K. G. Larsen, «A tutorial on Uppaal», in Proceedings of the International School on Formal Methods for the Design of Computer, Communication, and Software Systems, Springer, 2004, pp. 200-236.


Для цитирования:


Винарский Е.М., Захаров В.А. О моделировании последовательных реагирующих систем при помощи автоматов, работающих в реальном времени. Моделирование и анализ информационных систем. 2020;27(4):396-411. https://doi.org/10.18255/1818-1015-2020-4-396-411

For citation:


Vinarskii E.M., Zakharov V.A. On the Modeling of Sequential Reactive Systems by Means of Real Time Automata. Modeling and Analysis of Information Systems. 2020;27(4):396-411. (In Russ.) https://doi.org/10.18255/1818-1015-2020-4-396-411

Просмотров: 197


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)