О возможностях автоматного описания параллельной композиции временных автоматов

Конечные автоматы широко используются для анализа и синтеза дискретных систем. При описании систем, поведение которых зависит от времени, конечный автомат расширяется введением временных аспектов и вводится понятие временного автомата. В настоящей статье рассматривается проблема построения параллельной композиции для двух моделей временных автоматов, а именно, для автоматов с таймаутами и автоматов с временными ограничениями. Две эти формы временных автоматов не являются взаимозаменяемыми и являются более частными случаями общей модели временного автомата, содержащего как таймауты, так и временные ограничения. Мы также считаем, что все выше упомянутые модели временных автоматов имеют целочисленные выходные задержки (выходные таймауты). Автоматы-компоненты работают в режиме диалога, по завершении которого композиция выдаёт внешний выходной символ. При решении задач анализа для системы взаимодействующих конечных автоматов с использованием классических методов такая композиция обычно описывается единственным автоматом. В работе показывается, что в общем случае, в отличие от случая классических конечных автоматов, наличия «медленной внешней среды» и отсутствия осцилляций недостаточно для описания поведения композиции детерминированным автоматом с одной временной переменной, если входные символы могут поступать не только в целочисленные, но и рациональные моменты времени. Тем не менее, определяется класс систем, в которых каждое внешнее входное воздействие инициирует диалог между компонентами, что позволяет описать поведение такой композиции детерминированным автоматом с одной временной переменной. В частности, рассматривается последовательная композиция временных автоматов, которая удовлетворяет такому ограничению. Другое ограничение продиктовано наличием таймаутов, значение которого в каждом из состояний должно превышать величину выходной задержки при обработке любого перехода в этом состоянии.

конечный автомат, входные и выходные таймауты, временные ограничения, композиция

1. Гилл А. Введение в теорию конечных автоматов. М.: Издательство Наука, 1966, 272 с.

2. Rita Dorofeeva, Khaled El-Fakih, Stephane Maag, Ana R. Cavalli, Nina Yevtushenko FSM-based conformance testing methods: A survey annotated with experimental evaluation. Information and Software Technology, 2010, 52, pp. 1286-1297.

3. M. Merayo, M. Nunez, I. Rodriguez. Formal testing from timed finite state machines, Comput. Netw. 52 (2) (2008) 432–460.

4. El-Fakih K., Yevtushenko N., Simão A. A practical approach for testing timed deterministic finite state machines with single clock. Science of Computer Programming, Elsevier, 2014, Vol. 80, pp. 343–355.

5. Maxim Zhigulin, Nina Yevtushenko, Stéphane Maag, Ana R. Cavalli. FSM-Based Test Derivation Strategies for Systems with Time-Outs. Proc. of the 11th International Conference on Quality Software, QSIC2011, IEEE, 2011. pp. 141-149.

6. Larsen, K.G. Testing real-time embedded software using UPPAAL-TRON: an industrial case study. Proceedings of the 5th ACM international conference on Embedded software, 2005, pp. 299–306.

7. Bresolin D. Deterministic Timed Finite State Machines: Equivalence Checking and Expressive Power. Intern Conf. GANDALF, 2014, pp. 203–216.

8. Villa, T., Yevtushenko, N., Brayton, R.K., Mishchenko, A., Petrenko, A., Sangiovanni-Vincentelli, A. The Unknown Component Problem. Theory and Applications. Springer, 2012, 312 p.

9. Лапутенко А. В., Громов М. Л., Торгаев С. Н.. Реализация и тестирование системы сигнализации на баpе микроконтроллера STM32F407VG. Изв. вузов. Физика, 2016, Т. 59, № 12, стр. 174-176.

10. Gromov M., Tvardovskii A., Yevtushenko N. Testing Systems of interacting Timed Finite State Machines with the Guaranteed Fault Coverage. International Conference of Young Specialists on Micro/Nanotechnologies and Electron Devices, 2016, pp. 96–99.

11. Gromov M., Tvardovskii A., Yevtushenko N. Testing Components of Interacting Timed Finite State Machines. Proceedings of IEEE East-West Design & Test Symposium (EWDTS), 2016, pp. 193–196.

12. O. Kondratyeva, M. Gromov. To the Parallel Composition of Timed Finite State Machines. Proceedings of the 5th Spring/Summer Young Researches’ Colloquium on Software Engineering, 2011, pp. 94-99.

13. Alexandre Petrenko, Nina Yevtushenko, Gregor von Bochmann:

14. Fault Models for Testing in Context. FORTE 1996, pp. 163-178

15. Tripakis S. Folk Theorems on the Determinization and Minimization of Timed Automata. In: Larsen K.G., Niebert P. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2003. Lecture Notes in Computer Science, vol. 2791, pp. 222-226.