ITU

From Transition Systems to Variability Models and from Lifted Model Checking Back to UPPAAL

Research output: Conference Article in Proceeding or Book/Report chapterBook chapterResearchpeer-review

Standard

From Transition Systems to Variability Models and from Lifted Model Checking Back to UPPAAL. / Dimovski, Aleksandar; Wasowski, Andrzej.

Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday. Springer, 2017. p. 249-268 (Lecture Notes in Computer Science, Vol. 10460).

Research output: Conference Article in Proceeding or Book/Report chapterBook chapterResearchpeer-review

Harvard

Dimovski, A & Wasowski, A 2017, From Transition Systems to Variability Models and from Lifted Model Checking Back to UPPAAL. in Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday. Springer, Lecture Notes in Computer Science, vol. 10460, pp. 249-268. https://doi.org/10.1007/978-3-319-63121-9_13

APA

Dimovski, A., & Wasowski, A. (2017). From Transition Systems to Variability Models and from Lifted Model Checking Back to UPPAAL. In Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday (pp. 249-268). Springer. Lecture Notes in Computer Science Vol. 10460 https://doi.org/10.1007/978-3-319-63121-9_13

Vancouver

Dimovski A, Wasowski A. From Transition Systems to Variability Models and from Lifted Model Checking Back to UPPAAL. In Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday. Springer. 2017. p. 249-268. (Lecture Notes in Computer Science, Vol. 10460). https://doi.org/10.1007/978-3-319-63121-9_13

Author

Dimovski, Aleksandar ; Wasowski, Andrzej. / From Transition Systems to Variability Models and from Lifted Model Checking Back to UPPAAL. Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday. Springer, 2017. pp. 249-268 (Lecture Notes in Computer Science, Vol. 10460).

Bibtex

@inbook{594b4edb77a143579e282156c7b1eea5,
title = "From Transition Systems to Variability Models and from Lifted Model Checking Back to UPPAAL",
abstract = "Variational systems (system families) allow effective building of many custom system variants for various configurations. Lifted (family-based) verification is capable of verifying all variants of the family simultaneously, in a single run, by exploiting the similarities between the variants. These algorithms scale much better than the simple enumerative “brute-force” way. Still, the design of family-based verification algorithms greatly depends on the existence of compact variability models (state representations). Moreover, developing the corresponding family-based tools for each particular analysis is often tedious and labor intensive.In this work, we make two contributions. First, we survey the history of development of variability models of computation that compactly represent behavior of variational systems. Second, we introduce variability abstractions that simplify variability away to achieve efficient lifted (family-based) model checking for real-time variability models. This reduces the cost of maintaining specialized family-based real-time model checkers. Real-time variability models can be model checked using the standard UPPAAL. We have implemented abstractions as syntactic source-to-source transformations on UPPAAL input files, and we illustrate the practicality of this method on a real-time case study.Both authors are supported by The Danish Council for Independent Research under a Sapere Aude project, VARIETE.",
author = "Aleksandar Dimovski and Andrzej Wasowski",
year = "2017",
doi = "10.1007/978-3-319-63121-9_13",
language = "English",
isbn = "978-3-319-63120-2",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "249--268",
booktitle = "Models, Algorithms, Logics and Tools",
address = "Germany",

}

RIS

TY - CHAP

T1 - From Transition Systems to Variability Models and from Lifted Model Checking Back to UPPAAL

AU - Dimovski, Aleksandar

AU - Wasowski, Andrzej

PY - 2017

Y1 - 2017

N2 - Variational systems (system families) allow effective building of many custom system variants for various configurations. Lifted (family-based) verification is capable of verifying all variants of the family simultaneously, in a single run, by exploiting the similarities between the variants. These algorithms scale much better than the simple enumerative “brute-force” way. Still, the design of family-based verification algorithms greatly depends on the existence of compact variability models (state representations). Moreover, developing the corresponding family-based tools for each particular analysis is often tedious and labor intensive.In this work, we make two contributions. First, we survey the history of development of variability models of computation that compactly represent behavior of variational systems. Second, we introduce variability abstractions that simplify variability away to achieve efficient lifted (family-based) model checking for real-time variability models. This reduces the cost of maintaining specialized family-based real-time model checkers. Real-time variability models can be model checked using the standard UPPAAL. We have implemented abstractions as syntactic source-to-source transformations on UPPAAL input files, and we illustrate the practicality of this method on a real-time case study.Both authors are supported by The Danish Council for Independent Research under a Sapere Aude project, VARIETE.

AB - Variational systems (system families) allow effective building of many custom system variants for various configurations. Lifted (family-based) verification is capable of verifying all variants of the family simultaneously, in a single run, by exploiting the similarities between the variants. These algorithms scale much better than the simple enumerative “brute-force” way. Still, the design of family-based verification algorithms greatly depends on the existence of compact variability models (state representations). Moreover, developing the corresponding family-based tools for each particular analysis is often tedious and labor intensive.In this work, we make two contributions. First, we survey the history of development of variability models of computation that compactly represent behavior of variational systems. Second, we introduce variability abstractions that simplify variability away to achieve efficient lifted (family-based) model checking for real-time variability models. This reduces the cost of maintaining specialized family-based real-time model checkers. Real-time variability models can be model checked using the standard UPPAAL. We have implemented abstractions as syntactic source-to-source transformations on UPPAAL input files, and we illustrate the practicality of this method on a real-time case study.Both authors are supported by The Danish Council for Independent Research under a Sapere Aude project, VARIETE.

U2 - 10.1007/978-3-319-63121-9_13

DO - 10.1007/978-3-319-63121-9_13

M3 - Book chapter

SN - 978-3-319-63120-2

T3 - Lecture Notes in Computer Science

SP - 249

EP - 268

BT - Models, Algorithms, Logics and Tools

PB - Springer

ER -

ID: 82396684