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

View graph of relations

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
PublisherSpringer
Publication date2017
Pages249-268
ISBN (Print)978-3-319-63120-2
ISBN (Electronic)978-3-319-63121-9
DOIs
Publication statusPublished - 2017
SeriesLecture Notes in Computer Science
Volume10460
ISSN0302-9743

Downloads

No data available

ID: 82396684