Incremental model checking of delta-oriented software product lines

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