Compositional verification of real-time systems using Ecdar

A. David, K.G. Larsen, M.H. Møller, Ulrik Nyman, A.P. Ravn, A. Skou, A. Legay, A. Wasowski

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

13 Citationer (Scopus)
364 Downloads (Pure)

Abstrakt

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.
OriginalsprogEngelsk
TidsskriftInternational Journal on Software Tools for Technology Transfer
Vol/bind14
Udgave nummer6
Sider (fra-til)703-720
Antal sider18
ISSN1433-2779
DOI
StatusUdgivet - 15 jun. 2012

Fingeraftryk Dyk ned i forskningsemnerne om 'Compositional verification of real-time systems using Ecdar'. Sammen danner de et unikt fingeraftryk.

  • Citationsformater