by Lochau, Malte, Mennicke, Stephan, Baller, Hauke and Ribbeck, Lars
Abstract:
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 $\mu$-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.
Reference:
Incremental model checking of delta-oriented software product lines (Lochau, Malte, Mennicke, Stephan, Baller, Hauke and Ribbeck, Lars), In Journal of Logical and Algebraic Methods in Programming, volume 85, 2016.
Bibtex Entry:
@Article{Lochau2016,
Title = {{Incremental model checking of delta-oriented software product lines}},
Author = {Lochau, Malte and Mennicke, Stephan and Baller, Hauke and Ribbeck, Lars},
Journal = {Journal of Logical and Algebraic Methods in Programming},
Year = {2016},
Number = {1},
Pages = {245--267},
Volume = {85},
Abstract = {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 $\mu$-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.},
Doi = {10.1016/j.jlamp.2015.09.004},
ISSN = {23522216},
Keywords = {Model checking,Operational semantics,Variability modeling,imotep},
Mendeley-tags = {imotep},
Url = {http://www.sciencedirect.com/science/article/pii/S2352220815000863}
}