Д. Ю. Волканов, В. А. Захаров, Д. А. Зорин, И. В. Коннов, В. В. Подымов, “Как разработать простое средство верификации систем реального времени”, Модел. и анализ информ. систем, 2012, том 19, номер 6,страницы 45

Как разработать простое средство верификации систем реального времени

Д. Ю. Волканов^a, В. А. Захаров^a, Д. А. Зорин^a, И. В. Коннов^b, В. В. Подымов^a

^a Московский государственный университет им. М. В. Ломоносова
^b Technische Universität Wien

Аннотация: Исследуется задача верификации систем реального времени (СРВ). Для описания СРВ удобно использовать диаграммы состояний UML с семантикой, определяемой иерархическими автоматами. Для верификации СРВ часто применяется средство UPPAAL, разработанное для проверки формул логики TCTL на сети временных автоматов. Основным результатом данной статьи является алгоритм трансляции иерархических автоматов в сеть временных автоматов и обоснование его корректности.

Ключевые слова: верификация, система реального времени, диаграмма состояний, иерархический автомат, временной автомат.

УДК: 519.7

Поступила в редакцию: 22.07.2012