Family-Based Model Checking Without a Family-Based Model Checker

Aleksandar Dimovski, Ahmad Salim Al-Sibahi, Claus Brabrand, Andrzej Wasowski

    Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

    Abstract

    Many software systems are variational: they can be configured to meet diverse sets of requirements. Variability is found in both communication protocols and discrete controllers of embedded systems. In these areas, model checking is an important verification technique. For variational models (systems with variability), specialized family-based model checking algorithms allow
    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.
    Original languageEnglish
    Title of host publicationModel Checking Software : 22nd International Symposium, SPIN 2015, Stellenbosch, South Africa, August 24-26, 2015, Proceedings
    EditorsB. Fischer, J. Geldenhuys
    Number of pages18
    Volume9232
    PublisherSpringer
    Publication date14 Aug 2015
    Pages282-299
    ISBN (Print)978-3-319-23403-8
    DOIs
    Publication statusPublished - 14 Aug 2015
    Event22nd International SPIN Symposium on Model Checking of Software - Stellenbosch University, Stellenbosch, South Africa
    Duration: 24 Aug 201526 Aug 2015
    http://www.spin2015.org/

    Conference

    Conference22nd International SPIN Symposium on Model Checking of Software
    LocationStellenbosch University
    Country/TerritorySouth Africa
    CityStellenbosch
    Period24/08/201526/08/2015
    Internet address
    SeriesLecture Notes in Computer Science
    ISSN0302-9743

    Keywords

    • Family-Based Abstract Model Checking
    • Variability Abstractions
    • Model Checkers

    Fingerprint

    Dive into the research topics of 'Family-Based Model Checking Without a Family-Based Model Checker'. Together they form a unique fingerprint.

    Cite this