University of Twente Student Theses


Reducing UPPAAL models through control flow analysis

Slomp, G.H. (2010) Reducing UPPAAL models through control flow analysis.

[img] PDF
Abstract:This paper present a dead variable analysis algorithm for reducing the state space of UPPAAL models. By resetting irrelevant variables to their initial value reductions of UPPAAL models are achieved. The developed algorithm consists of two parts. In the rst part we dene an algorithm to determine the relevance of variables. We also cope with the various features of UPPAAL like, for instance, function calls and value passing variables and we present an algorithm to determine the relevance of variables that are used in a property. In the second part we transform the original timed automata by introducing resets for irrelevant variables. We improve on extending transformation algorithms by not resetting irrelevant variables at every location. Based on the developed algorithm we implemented a tool that performs the transformation and by executing this tool for three case studies we show that it indeed achieves reductions. We conclude with noting that, next to the reductions, the main benet of our work is that UPPAAL users do not have to perform the resets manually any more, making their work easier and less error prone, as these resets can now be performed automatically.
Item Type:Essay (Master)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science MSc (60300)
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page