Optimizations for UPPAAL

Synopsis:

The subject of this report is verification of software in the context of Uppaal. This report is a result of a graduate pro ject con- cerning the investigation of areas and theory of interest, for the purpose of improving the verification efforts of the verification tool Uppaal. Traditionally program slicing has been suggested for many applications, but these areas has primarily been related to testing or debugging of imperative languages, we show how to use slicing to reduce the syntactic size of a Uppaal model in order to reduce the size of the corresponding state-space which should be explored during verification of some property. We re-introduce known theory from software verification research in order to apply it to timed automata which is the underlying model for the Uppaal tool. Furthermore, we provide the algorithm for applying the slicing technique for Uppaal. A full semantics for the Uppaal verification tool has never been given and we therefore provide the semantics for the timed automata of Uppaal and the complete semantics is planed as future work. An intuition behind predicate abstraction and why this technique could be interesting in the context of Uppaal is also presented.