From Transition Systems to Variability Models and from Lifted Model Checking Back to UPPAAL
Research output: Conference Article in Proceeding or Book/Report chapter › Book chapter › Research › peer-review
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.
|Title of host publication||Models, Algorithms, Logics and Tools : Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday|
|Publication status||Published - 2017|
|Series||Lecture Notes in Computer Science|