|
ИСТИНА |
Войти в систему Регистрация |
Интеллектуальная Система Тематического Исследования НАукометрических данных |
||
On the designing of model checkers for real-time distributed systemsдоклад на конференции
- Авторы: Коннов И.В., Подымов В.В., Зорин Д.А., Захаров В.А., Yu D.V.
- Международная Конференция : Семинар "Программные семантики, спецификации и верификация (PSSV)"
- Даты проведения конференции: 2012
- Тип доклада: Устный
- Докладчик: не указан
- Место проведения: Нижний Новгород
-
Аннотация доклада:
To verify real-time properties of UML statecharts one may apply a UPPAAL, toolbox for model checking of real-time systems. One of the most suit- able ways to specify an operational semantics of UML statecharts is to invoke the formal model of Hierarchical Timed Automata. Since the model language of UP- PAAL is based on Networks of Timed Automata one has to provide a conversion of Hierarchical Timed Automata to Networks of Timed Automata. In this paper we describe this conversion algorithm and prove that it is correct w.r.t. UPPAAL query language which is based on the subset of Timed CTL.
- Добавил в систему: Зорин Даниил Александрович