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

Aleksandar Dimovski, Andrzej Wasowski

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


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.
Original languageEnglish
Title of host publicationModels, Algorithms, Logics and Tools : Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday
Publication date2017
ISBN (Print)978-3-319-63120-2
ISBN (Electronic)978-3-319-63121-9
Publication statusPublished - 2017
SeriesLecture Notes in Computer Science


Dive into the research topics of 'From Transition Systems to Variability Models and from Lifted Model Checking Back to UPPAAL'. Together they form a unique fingerprint.

Cite this