@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}
}