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

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

Aalborg Universitet

Publikation: Artikel i tidsskrift og konference artikel i tidsskrift › Tidsskriftartikel › Forskning › peer 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.

Originalsprog	Engelsk
Tidsskrift	International Journal on Software Tools for Technology Transfer
Vol/bind	14
Udgave nummer	6
Sider (fra-til)	703-720
ISSN	1433-2779
Status	Udgivet - 2012

Emneord

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

MT-Lab - Modelling of Information Technology
Wasowski, A. (CoI), Godskesen, J. C. (PI), Song, L. (CoI), Traonouez, L.-M. (CoI) & Biondi, F. (CoI)
01/11/2008 → 31/10/2013
Projekter: Projekt › Forskning

Citationsformater

@article{0fed01f29af74c3c82a249880f53327a,

title = "Compositional verification of real-time systems using Ecdar",

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.",

keywords = "Timed input/output automata, Compositional verification, Real-time systems, Leader election protocol, Timed input/output automata, Compositional verification, Real-time systems, Leader election protocol",

author = "Alexandre David and Larsen, {Kim Guldstrand} and Axel Legay and M{\o}ller, {Mikael Harkj{\ae}r} and Nyman, {Ulrik Mathias} and Ravn, {Anders Peter} and Skou, {Arne Joachim} and Andrzej Wasowski",

year = "2012",

language = "English",

volume = "14",

pages = "703--720",

journal = "International Journal on Software Tools for Technology Transfer",

issn = "1433-2779",

publisher = "Springer",

number = "6",

}

TY - JOUR

T1 - Compositional verification of real-time systems using Ecdar

AU - David, Alexandre

AU - Larsen, Kim Guldstrand

AU - Legay, Axel

AU - Møller, Mikael Harkjær

AU - Nyman, Ulrik Mathias

AU - Ravn, Anders Peter

AU - Skou, Arne Joachim

AU - Wasowski, Andrzej

PY - 2012

Y1 - 2012

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

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

KW - Timed input/output automata

KW - Compositional verification

KW - Real-time systems

KW - Leader election protocol

KW - Timed input/output automata

KW - Compositional verification

KW - Real-time systems

KW - Leader election protocol

M3 - Journal article

SN - 1433-2779

VL - 14

SP - 703

EP - 720

JO - International Journal on Software Tools for Technology Transfer

JF - International Journal on Software Tools for Technology Transfer

IS - 6

ER -

Compositional verification of real-time systems using Ecdar

Abstract

Emneord

Fingeraftryk

Projekter

MT-Lab - Modelling of Information Technology

Citationsformater