Diagnostic model-checking for real-time systems

  • Kim G. Larsen
  • , Paul Pettersson
  • , Wang Yi

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

25 Scopus citations

Abstract

UPPAAL is a new tool suit for automatic verification of networks of timed automata. In this paper we describe the diagnostic model-checking feature of UPPAAL and illustrates its usefulness through the debugging of (a version of) the Philips Audio-Control Protocol. Together with a graphical interface of UPPAAL this diagnostic feature allows for a number of errors to be more easily detected and corrected.

Original languageEnglish
Title of host publicationHybrid Systems III - Verification and Control
EditorsRajeev Alur, Thomas A. Henzinger, Eduardo D. Sontag
PublisherSpringer Verlag
Pages575-586
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 'Diagnostic model-checking for real-time systems'. Together they form a unique fingerprint.

Cite this