WG211/M10Schaefer

Deductive Verification of Software Product Lines by Ina Schaefer

A software product line consists is a family of program variants that
are developed from a common code base. In particular, for
safety-critical or business-critical applications, product quality and
correctness has to be rigorously ensured. Analyzing each product variant
in isolation is in general infeasible, since the number of product
variants is exponential in the number of product features.

In my talk, I present efficient deductive program verification
techniques for delta-oriented software product lines. Delta-oriented
programming is a modular, yet flexible way to describe a family of
program variants. Besides type-safety of delta-oriented product lines,
our verification techniques consider functional correctness properties
specified using design-by-contract. If product variability is restricted
suitably, compositional family-based verification can establish
correctness of all product variants by analyzing the product line code
base only once. Without any restrictions on product variability,
incremental product-based verification techniques reduce verification
effort by progressing from one verified program variant to the next. In
between both extrems, constraint-based verification techniques provide a
compromise between the family-based and product-based verification
approaches and allow relaxing the restrictions on the admissible product
variability.