Compositional verification of real-time systems using Ecdar

Publication: Research - peer-reviewJournal article

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.
Close

Details

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
Number of pages18
ISSN1433-2779
DOI
StatePublished - 15 Jun 2012

Download statistics

No data available
ID: 65653879