Incremental model checking of delta-oriented software product lines

TitleIncremental model checking of delta-oriented software product lines
Publication TypeJournal Article
Year of Publication2016
AuthorsLochau, M., S. Mennicke, H. Baller, and L. Ribbeck
Refereed DesignationRefereed
JournalJournal of Logical and Algebraic Methods in Programming
Start Page245
Date Published01/2016

We propose DeltaCCS, a delta-oriented extension to Milner's process calculus CCS to formalize behavioral variability in software product line specifications in a modular way. In DeltaCCS, predefined change directives are applied to core process semantics by overriding the CCS term rewriting rule in a determined way. On this basis, behavioral properties expressed in the Modal μ-Calculus are verifiable for entire product-line specifications both product-by-product as well as in a family-based manner as usual. To overcome potential scalability limitations of those existing strategies, we propose a novel approach for incremental model checking of product lines. Therefore, variability-aware congruence notions and a respective normal form for DeltaCCS specifications allow for a rigorous local reasoning on the preservation of behavioral properties after varying CCS specifications. We present a prototypical DeltaCCS model checker implementation based on Maude and provide evaluation results obtained from various experiments concerning efficiency trade-offs compared to existing approaches.