- Об институте
- Инновации
- Структура
- Отдел "Архитектуры вычислительных систем"
- Отдел "Информационных систем"
- Отдел "Компиляторных технологий"
- Отдел "Системного программирования"
- Отдел "Системной интеграции и прикладных программных комплексов"
- Отдел "Теоретической информатики"
- Отдел "Технологий программирования"
- Ученый совет
- Диссертационный совет
- Центр верификации ОС Linux
- Исследовательский центр доверенного искусственного интеллекта
- Центр компетенции по параллельным и распределенным вычислениям
- Образование
- Издания
- Новости
- Лицензии
Как разработать простое средство верификации систем реального времени.
Авторы
Волканов Д.Ю., Захаров В.А., Зорин Д.А., Коннов И.В., Подымов В.В.
Аннотация
Исследуется задача верификации систем реального времени (СРВ). Для описания СРВ удобно использовать диаграммы состояний UML с семантикой, определяемой иерархическими автоматами. Для верификации СРВ часто применяется средство UPPAAL, разработанное для проверки формул логики TCTL на сети временных автоматов. Основным результатом данной статьи является алгоритм трансляции иерархических автоматов в сеть временных автоматов и обоснование его корректности.
Полный текст статьи в формате pdfКлючевые слова
верификация, система реального времени, диаграмма состояний, иерархический автомат, временной автомат
Издание
Моделирование и анализ информационных систем, 2012, том 19, № 6, с. 45-56.