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.
|Tidsskrift||International Journal on Software Tools for Technology Transfer|
|Status||Udgivet - 15 jun. 2012|
David, A., Larsen, K. G., Møller, M. H., Nyman, U., Ravn, A. P., Skou, A., Legay, A., & Wasowski, A. (2012). Compositional verification of real-time systems using Ecdar. International Journal on Software Tools for Technology Transfer, 14(6), 703-720. https://doi.org/10.1007/s10009-012-0237-y