Идентификация финального состояния в автоматах с таймаутами и временными ограничениями
https://doi.org/10.15514/ISPRAS-2026-38(4)-16
Аннотация
В статье вводятся понятия установочной и синхронизирующей последовательностей для конечных автоматов с временными ограничениями и таймаутами. Такие последовательности широко используются для идентификации финального состояния исследуемого автомата как при синтезе тестов на основе формальных моделей, так и при обучении конечно-автоматных моделей. Метод синтеза установочных и синхронизирующих последовательностей основан на использовании конечно-автоматной абстракции временного автомата, поскольку методы синтеза таких идентификационных последовательностей по конечно-автоматной модели хорошо изучены.
Об авторах
Александр Сергеевич ТВАРДОВСКИЙ
Национальный исследовательский Томский государственный университет
Россия
Россия
Кандидат физико-математических наук, доцент ТГУ. Научные интересы: формальные спецификации, генерация тестов, системы реального времени, теория автоматов.
Игорь Борисович БУРДОНОВ
Институт системного программирования РАН им. В.П. Иванникова
Россия
Россия
Доктор физико-математических наук, главный научный сотрудник ИСП РАН. Научные интересы: формальные спецификации, генерация тестов, технология компиляции, системы реального времени, операционные системы, объектно-ориентированное программирование, сетевые протоколы, процессы разработки программного обеспечения.
Нина Владимировна ЕВТУШЕНКО
Институт системного программирования РАН им. В.П. Иванникова, Национальный исследовательский университет «Высшая школа экономики»
Россия
Россия
Доктор технических наук, профессор, главный научный сотрудник ИСП РАН, до 1991 года работала научным сотрудником в Сибирском физико-техническом институте. С 1991 г. работала в ТГУ профессором, зав. кафедрой, зав. лабораторией по компьютерным наукам. Её исследовательские интересы включают формальные методы, теорию автоматов, распределённые системы, протоколы и тестирование программного обеспечения.
Список литературы
1. Moore E. F. Gedanken-experiments on sequential machines. Automata Studies (Annals of Mathematical Studies), 1956, 1, pp. 129-153.
2. Гилл А. Введение в теорию конечных автоматов. Наука, 1966.
3. Hibbard T.N. Least upper bounds on minimal terminal state experiments of two classes of sequential machines. J. ACM, 8, 1961, pp. 601-612.
4. Kohavi Z. Switching and Finite Automata Theory, McGraw-Hill, 1978.
5. D. Lee, M. Yannakakis. Testing Finite-State Machines: State Identification and Verification. IEEE Transactions on Computers, 1994, 43(3), pp. 306-320.
6. Sandberg S. Homing and Synchronizing Sequences. Lecture Notes in Computer Science, 2005, 3472, pp. 5-33.
7. Н.В. Евтушенко, Н.Г. Кушик. Некоторые задачи идентификации состояний для недетерминированных автоматов. Томск, 2018.
8. Hennie F.C. Fault detecting experiments for sequential circuits. Proc. of the 5th Annual Symposium on Circuit Theory and System Design, 1965, pp. 95-100.
9. Chow T. S. Testing software Design Modelled by Finite State Machines. IEEE Trans. Software Eng., 1978, 4(3), pp. 178-187.
10. Lee, D., Yannakakis, M. Principles and methods of testing finite state machines-a survey. Proceedings of the IEEE, 1996, 8, 4(8), pp.1090-1123.
11. Bochmann G. and Petrenko A. Protocol testing: review of methods and relevance for software testing. Proccedings of the 1994 ACM International Symposium on Software Testing and Analysis (ISSTA’94), pp. 109-124.
12. Kushik, N., López, J., Cavalli, A. and Yevtushenko, N. Improving Protocol Passive Testing through “Gedanken” Experiments with Finite State Machines. Proceedings of Intern. Conf. Quality, Reliability and Security, 2016, pp 315-322.
13. R.L. Rivest and R.E. Schapire. Inference of finite automata using homing sequences. Inf. Comput., 1993, 103(2), pp. 299–347.
14. Roland Groz, Nicolas Br´emond, Adenilso da Silva Simao, and Catherine Oriat Winference: A heuristic approach to retrieve models through black box testing. J. Syst. Softw.,2020, 159.
15. Loes Kruger, Bharat Garhewal, Frits Vaandrager. Lower Bounds for Active Automata Learning. Proceedings of 16th edition of the International Conference on Grammatical Inference, 2023.
16. Yennigun H., Yevtushenko N., Kushik N. and López, J. The effect of partiality and adaptivity on the complexity of FSM state identification problems. Труды ИСП РАН, 2018, том 3, pp. 1-14
17. Alur, R, and Dill. D. L. A Theory of Timed automata. Theoretical Computer Science,1994, 126(2), pp.183¬-235.
18. Merayo M. G., Nunez, M., Rodriguez I.: Formal Testing from Timed Finite State Machines. Computer Networks, 2008, 52 (2), pp. 432–460 (2008)
19. Springintveld J, Vaandrager F, D'Argenio P (2001) Testing timed automata. Theoretical Computer Science, 2001, 254(1-2), pp. 225–257.
20. Bresolin D, El-Fakih K, Villa T., Yevtushenko N. Equivalence checking and intersection of deterministic timed finite state machines. Formal Methods Syst. Des. 59(1), 2021, pp. 77-102.
21. Tvardovskii A, Yevtushenko N. Deriving homing sequences for Finite State Machines with timed guards. Automatic Control and Computer Sciences, 2021, 55 (7), pp. 738–750.
22. Tvardovskii A, Yevtushenko N. Deriving homing sequences for Finite State Machines with timeouts. Comput. Journal, 2023, 66 (9), pp. 2181-2190.
Рецензия
Для цитирования:
ТВАРДОВСКИЙ А.С., БУРДОНОВ И.Б., ЕВТУШЕНКО Н.В. Идентификация финального состояния в автоматах с таймаутами и временными ограничениями. Труды Института системного программирования РАН. 2026;38(4):7-22. https://doi.org/10.15514/ISPRAS-2026-38(4)-16
For citation:
TVARDOVSKII A.S., BURDONOV I.B., YEVTUSHENKO N.V. Final State Identification of Finite State Machines with Timeouts and Timed Guards. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2026;38(4):7-22. (In Russ.) https://doi.org/10.15514/ISPRAS-2026-38(4)-16
Послать статью по эл. почте 