Compositional verification of real-time systems using Ecdar

Alexandre David, Kim Guldstrand Larsen, Axel Legay, Mikael Harkjær Møller, Ulrik Mathias Nyman, Anders Peter Ravn, Arne Joachim Skou, Andrzej Wasowski

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

Abstract

We present a specification theory for timed systems implemented in the ECDAR tool. We illustrate the operations of the specification theory on a running example, showing the models and verification checks. To demonstrate the power of the compositional verification, we perform an in depth case study of a leader election protocol; Modeling it in ECDAR as Timed input/output automata Specifications and performing both monolithic and compositional verification of two interesting properties on it. We compare the execution time of the compositional to the classical verification showing a huge difference in favor of compositional verification.
Original languageEnglish
JournalInternational Journal on Software Tools for Technology Transfer
Volume14
Issue number6
Pages (from-to)703-720
ISSN1433-2779
Publication statusPublished - 2012

Keywords

  • Timed input/output automata
  • Compositional verification
  • Real-time systems
  • Leader election protocol

Fingerprint

Dive into the research topics of 'Compositional verification of real-time systems using Ecdar'. Together they form a unique fingerprint.

Cite this