The tool Verifix is used for robust reachability analysis of timed automata. The input format for the tool is in the XML format, compatible with the Uppaal tool. The tool has been written in C++ and the source code has about 5.6 Klocs. Internally it uses the Uppaal DBM Library and the Uppaal Timed Automata Parser Library.


The executable binary file compiled under Linux with 64 bit can be dowloaded here (12Mb): verifix
The source code of the program can be dowloaded here: sources
The specifications with which the tool was tested can be downloaded here:
The Uppaal Timed Automata Parser Library needed minor header inclusion modifications. The modified version can be dowloaded here: