Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
10333451 | Journal of Logical and Algebraic Methods in Programming | 2016 | 23 Pages |
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 μ-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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Malte Lochau, Stephan Mennicke, Hauke Baller, Lars Ribbeck,