Uppaal Timed Automata Static Analysis library (UTASA)UTASA is a library created by Uffe Sørensen and myself, as a part of our master project. UTASA is a prototype implementation, in C++, of static analysis, algorithms and data structures, used for slicing models for the Uppaal modeling and verification tool. |
Slicing for Uppaal:The focus of this project (and the thesis) is to introduce slicing for Uppaal. Slicing is a technique based on static analysis used to reduce the syntactic size of models or applications. In this thesis, we show how slicing may be used to construct reachability preserving reductions of Uppaal models possibly improving the performance of the tool. Using automated slicing in Uppaal will eliminate the need for users to manually optimize models for faster verification of a certain property. Moreover, it allows less experienced users of Uppaal, which unknowingly may design models, containing unnecessary large amounts of data, to verify properties which \uppaal otherwise would have been unable to check.The slicing is done by analyzing the control-flow of a model, in order to extract dependencies between its components, which is then stored in a data structure known as a system dependency graph (SDG). Computing the relevant components (the slicing set) of the model is then achieved using graph analysis on the SDG. The sliced model is then constructed using only the components included in the slicing set. In order to formally define and prove correctness of the slicing approach, we define an extended notion of the timed automata formalism, which constitutes a non-trivial subset of the modeling language used in Uppaal. Moreover, to stress the complexity of verifying properties for Uppaal models and further motivate the use of slicing, the general problem of model-checking is described and known theory is presented. Finally, a prototype implementation of slicing for Uppaal has been developed to show that the slicing approach presented can in-fact be extended to the complete language of Uppaal. The prototype has been used to conduct a set of experiments, in which we succeeded in finding a design flaw in a model provided by students from the department of communication technology at AAU. Moreover, the experiments indicate that slicing does indeed provide an effective and beneficial component for \uppaal, which leads us to encourage the further development of the prototype towards inclusion in the offical distributed version of Uppaal. Resources:
Puplications
HOWTO - RequirementsThe pre-compiled version of TASlicer, is compiled for Linux (tested on RH enterprise and Debian) and OSX (intel 10.4) running the TASlicer app is a simple matter: ./TASlicer-32 my-train-gate.xml my-sliced-train-gate.xml - will produce a slice preserving all reachability properties. ./TASlicer-32 (with no arguments) will show usage ./TAslicer-32 --about will give you a small description of the tool. Compiling the source code for UTASA requires UTAP (uppaal timed automata parser) library (version 0.91), which means that UTASA inherits the same set of dependencies. UTAP can be download at http://www.cs.auc.dk/~behrmann/utap/ but currently comes with the following requirements: You need the following tools and libraries on your system in order to compile and use the library:
libutap uses automake and autoconf to generate make files and configure the build process. To configure and install the library, simply run: ./configure make # make install - UTASA does not require installation of UTAP You may want to specify an alternative installation path using the --prefix option. Having compiled UTAP, copy the library file, libutap.a from the src dir in UTAP to the src dir in UTASA, and repeat the build procedure for UTASA. |