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

Authors

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

DOI:

https://doi.org/10.7146/brics.v3i58.18769

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.

Downloads

Published

1996-06-28

How to Cite

Bengtsson, J., Larsen, K. G., 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