Further Reading - Model-Driven and Software Product Line Engineering - page 237

in recent work. Verification and validation of requirements
engineering is important to increase reliability and adequacy
of software systems.
Feature model verification and validation is a recent and
active area of research; several directions are successful
and important progress has been made in this context.
As it concerns mainly requirements, early verification and
validation solutions are preferable. Requirement reviews or
natural language analysis can be used to validate feature
models. As already said, the AMPLE approach [RAS 11]
suggests a way to analyze, organize, and extract a feature
model for requirements in natural languages. This provides
a valuable tool and an approach allowing validation from the
stakeholders.
Onesurveyabouttheanalysesoffeaturemodelsis[BEN06].
Obviously, the verification of feature models depends on
the complexity of the notations; for instance, cardinality,
constraint, or group concepts introduces more difficulties.
Verification of feature models is an issue explored by several
researchers,mainlyusingconstraintprogramming,description
logic, BDD, and satisfiability techniques. In [BAT 06], the
authors present some of the main challenges. Of course we
need automatic and efficient techniques. General properties
such as completeness or consistency can be formulated and
sometimes proved over formally specified systems. Techniques
such as formal proofs or model-checking can be used as soon as
the system is formally specified.As the feature model is close to
propositionalorfirst-orderlogic,severalattemptsweremadeto
use formal declarative languages or OCL and associated tools.
Czarnecki and Pietroszek [CZA 06] propose to analyze
feature-based model templates, that is, a feature model and an
annotated UML model describing additional semantics of the
feature model. They use a translation into OCL expressions of
the template model and a SAT solver to automatically check
that configured instances are compliant with the template's