TY - JOUR
T1 - Compositional verification of real-time systems using Ecdar
AU - David, A.
AU - Larsen, K.G.
AU - Møller, M.H.
AU - Nyman, Ulrik
AU - Ravn, A.P.
AU - Skou, A.
AU - Legay, A.
AU - Wasowski, A.
PY - 2012/6/15
Y1 - 2012/6/15
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.
UR - http://www.scopus.com/inward/record.url?scp=84861953803&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84861953803&partnerID=8YFLogxK
U2 - 10.1007/s10009-012-0237-y
DO - 10.1007/s10009-012-0237-y
M3 - Journal article
AN - SCOPUS:84867404484
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 -