UPPAAL-a tool suite for automatic verification of real-time systems

  • Johan Bengtsson
  • , Kim Larsen
  • , Fredrik Larsson
  • , Paul Pettersson
  • , Wang Yi

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

557 Scopus citations

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.does. uu. se/docs/rtmv/uppaal.

Original languageEnglish
Title of host publicationHybrid Systems III - Verification and Control
EditorsRajeev Alur, Thomas A. Henzinger, Eduardo D. Sontag
PublisherSpringer Verlag
Pages232-243
Number of pages12
ISBN (Print)354061155X, 9783540611554
DOIs
StatePublished - 1996
Externally publishedYes
Event5th DIMACS/SYCON Workshop on Verification and Control of Hybrid Systems, 1995 - New Brunswick, United States
Duration: 22 Oct 199525 Oct 1995

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1066
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference5th DIMACS/SYCON Workshop on Verification and Control of Hybrid Systems, 1995
Country/TerritoryUnited States
CityNew Brunswick
Period22/10/9525/10/95

Fingerprint

Dive into the research topics of 'UPPAAL-a tool suite for automatic verification of real-time systems'. Together they form a unique fingerprint.

Cite this