И. Монахов (АФТУ)
О верификации и управлении систем реального времени

Моделирование сложных систем, таких как встроенные системы или коммуникационные протоколы, часто требует умения выражать количественные ограничения по времени между событиями
(например, "задержка передачи составляет не более 5 мс"), поскольку корректность таких систем сильно зависит от этих численных соотношений.

ВременнЫе автоматы (Timed automata) были предложены в начале 90х годов в качестве модели для систем реального времени с довольно хорошими теоретическими свойствами. С тех пор они были хорошо изучены, и были так же разработаны средства, предназначенные для автоматического анализа этой модели.

На семинаре будут представлены основы верификации для модели Временного автомата.