ИСТИНА |
Войти в систему Регистрация |
|
ИСТИНА ИНХС РАН |
||
In this paper we present a tool to transform UML statecharts to UPPAAL automata. The tool allows one to check temporal properties against statecharts modeling a real-time system. We give the constraints on statecharts, the tool description, and the results of its application to a well-known traffic control real-time system.