Family-Based Model Checking Without a Family-Based Model Checker
Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review
efficient verification of multiple variants, simultaneously. These algorithms scale much better than ``brute force'' verification of individual systems, one-by-one. Nevertheless, they can deal with only very small variational models.
We address two key problems of family-based model checking. First, we improve scalability by introducing abstractions that simplify variability. Second, we reduce the burden of maintaining specialized family-based model checkers, by showing how the presented variability abstractions can be used to model-check variational models using the standard version of (single system) SPIN. The abstractions are first defined as Galois connections on semantic domains. We then show how to translate them into syntactic source-to-source transformations on variational models. This allows the use of SPIN with all its accumulated optimizations for efficient verification of variational models without any knowledge about variability. We demonstrate the practicality of this method on several examples using both the SNIP (family based) and SPIN (single system) model checkers.
|Title of host publication||Model Checking Software : 22nd International Symposium, SPIN 2015, Stellenbosch, South Africa, August 24-26, 2015, Proceedings|
|Editors||B. Fischer, J. Geldenhuys|
|Number of pages||18|
|Publication date||14 Aug 2015|
|Publication status||Published - 14 Aug 2015|
|Event||22nd International SPIN Symposium on Model Checking of Software - Stellenbosch University, Stellenbosch, South Africa|
Duration: 24 Aug 2015 → 26 Aug 2015
|Conference||22nd International SPIN Symposium on Model Checking of Software|
|Periode||24/08/2015 → 26/08/2015|
|Series||Lecture Notes in Computer Science|
- Family-Based Abstract Model Checking, Variability Abstractions, Model Checkers