Automatically transforming and relating Uppaal models of embedded systems

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 t multiple levels of abstraction, and timed trace inclusion is one way to relate the models. It is known that a deterministic and -free timed automaton can be transformed such that reachability analysis can decide timed trace inclusion with another timed automaton. Performing the transformation manually is tedious and error-prone. We have developed a tool that does it automatically for a large subset of Uppaal models. Certain features of the Uppaal modeling language, namely selection bindings and channel arrays, complicate the transformation. We formalize these features and extend the validation technique to incorporate them. We find it impracticable to manipulate some forms of channel array subscripts, and some combinations of selection bindings and universal qua...

• Type: Conference
• Year: 2008
• Where: EMSOFT
• Authors: Timothy Bourke, Arcot Sowmya
• Keywords: -free Timed Automaton, Channel Array, EMSOFT 2008, Software Engineering, Timed Trace Inclusion