UPPAAL—a Tool Suite for Automatic Verification of Real–Time Systems

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

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.
Published
1996-06-28
How to Cite
Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., & Yi, W. (1996). UPPAAL—a Tool Suite for Automatic Verification of Real–Time Systems. BRICS Report Series, 3(58). https://doi.org/10.7146/brics.v3i58.18769