Efficient Implementation of Model-Checkers for Networks of Timed Automata

Fredrik Larsson

May 2000

Abstract:

Since real-time systems often operate in safety-critical environments it is extremely important that they function correctly. uppaal is a tool that can be used for validation and verification of real-time systems. The user models the system using networks of timed automata and uses a simple logic to express safety requirements that the modelled system must satisfy to guarantee its correct behaviour. uppaal then performs reachability analysis using constraint solving techniques to check if the model satisfies the given requirements. In addition, the tool is also able to provide the user with a sample execution that explains why a requirement is (or is not) satisfied by the model. The analysis is fully automated.

This thesis describes various techniques adopted when implementing uppaal. Some of he techniques have improved the performance of uppaal significantly. We have studied the techniques with performance measurements in several case-studies. One of the main contributions is the comparison of different strategies in implementing the basic data structures and searching algorithms. The measurements can be used as hints on what parts of the model-checker that are most important to optimise. Though the techniques are studied in the context of timed automata, we believe that they are applicable to the implementation of general software tools for automated analysis.

Available as Postscript (1.2 MB), compressed Postscript (289 kB), and PDF (622 kB)

Download BibTeX entry.