Title :
Model Checking of Domain Artifacts in Product Line Engineering
Author :
Lauenroth, Kim ; Pohl, Klaus ; Toehning, S.
Author_Institution :
Software Syst. Eng., Univ. of Duisburg-Essen, Essen, Germany
Abstract :
In product line engineering individual products are derived from the domain artifacts of the product line. The reuse of the domain artifacts is constraint by the product line variability. Since domain artifacts are reused in several products, product line engineering benefits from the verification of domain artifacts. For verifying development artifacts, model checking is a well-established technique in single system development. However, existing model checking approaches do not incorporate the product line variability and are hence of limited use for verifying domain artifacts. In this paper we present an extended model checking approach which takes the product line variability into account when verifying domain artifacts. Our approach is thus able to verify that every permissible product (specified with I/O-automata) which can be derived from the product line fulfills the specified properties (specified with CTL). Moreover, we use two examples to validate the applicability of our approach and report on the preliminary validation results.
Keywords :
automata theory; formal specification; CTL; I/O-automata; development artifact verification; domain artifact verification; domain artifacts; model checking; product line engineering; product line variability; single system development; Automotive engineering; Design engineering; Formal verification; Quality assurance; Rails; Software engineering; Software systems; Software testing; Systems engineering and theory; Traffic control; Domain Artifact Verification; Model Checking; Product Line Engineering; Variability;
Conference_Titel :
Automated Software Engineering, 2009. ASE '09. 24th IEEE/ACM International Conference on
Conference_Location :
Auckland
Print_ISBN :
978-1-4244-5259-0
Electronic_ISBN :
1938-4300
DOI :
10.1109/ASE.2009.16