Automatically transforming and relating Uppaal models of embedded systems
Timothy Bourke, Arcot Sowmya · 2008
Relations between models are important for effective automatic validation, for comparing implementations with specifications, and for increased understanding of embedded systems designs. Timed automata may be used to model a system at multiple levels of abstraction, and timed trace inclusion is one way to relate the models.