Uppaal

Uppaal is a comprehensive software application that allows you to design, validate and verify real-time systems modelled as networks of timed automata. It is developed in Java and wrapped in a user-friendly workspace.

There is no setup pack involved, which makes Uppaal almost portable. Provided that you have Java installed on your computer, you can save the program files to any part of the disk and just click the JAR file to launch the tool.

Another possibility is to save it to a pen drive to directly run it on any PC with Java installed. An important aspect worth taking into account is that it does not modify Windows registry settings or create extra files on the disk without your permission.

The GUI is made from a single window split into three tabs for editing, simulating and verifying the project. The editor is split into two frames for navigating project parts (e.g. declarations, templates) and writing code, the simulator investigates and validates possible dynamic executions of a system during modelling, while the verification tool facilitates an overview on the project, thus enabling you to write queries and comments.

It is possible to zoom in and out, hide labels, reload the simulator, snap to grid, check and convert the syntax, change the search order (breadth first, depth first, random depth first), choose the state space reduction and representation, pick the diagnostic trace, extrapolation and hash table size, and more.

We have not come across any stability issues in our tests, since Uppaal did not hang, crash or pop up error messages. It has a good response time and minimal impact on system performance, so it doesn't hog CPU and RAM.

Uppaal comes in handy to students who want to work in an integrated environment for modelling, validating and verifying real-time systems.