UPPAAL - a Tool Suite for Automatic Verification of Real-Time Systems

Johan Bengtsson
Kim G. Larsen
Fredrik Larsson
Paul Pettersson
Wang Yi

December 1996

Abstract:

UPPAAL is a tool suite for automatic verification of safety and bounded liveness properties of real-time systems modeled as networks of timed automata. It includes: a graphical interface that supports graphical and textual representations of networks of timed automata, and automatic transformation from graphical representations to textual format, a compiler that transforms a certain class of linear hybrid systems to networks of timed automata, and a model-checker which is implemented based on constraint-solving techniques. UPPAAL also supports diagnostic model-checking providing diagnostic information in case verification of a particular real-time systems fails.

The current version of UPPAAL is available on the World Wide Web via the UPPAAL home page http://www.docs.uu.se/docs/rtmv/uppaal

Available as PostScript, PDF.

 

Last modified: 2003-06-08 by webmaster.