Dynamic Consistency Checking of Domain Requirements in Product Line Engineering

The domain requirements specification (DRS) of a product line comprises the common and variable requirements of all products of the product line. Due to the variability defined for a product line, the DRS may contain contradicting requirements. For example, it may contain requirements A and not(A) which can be included in different products. Checking the consistency of DRS in product line engineering is thus not straightforward. Variability information has to be incorporated into the consistency checks to ensure that contradicting requirements do not become part of the same product requirements specification. In this paper, we present a consistency checking technique for dynamic properties of DRS based on model checking techniques. We present a proof of correctness for the technique, sketch our tool environment, and report on the application of the approach to an industrial example.