May 15th, 2014 Compositional Verification of Software Product Lines

  • Speaker: Ina Schaefer
  • Title: Compositional Verification of Software Product Lines
  • Abstract: Software product line engineering allows large software systems to be developed and adapted for varying customer needs. The products of a software product line can be described by means of a hierarchical variability model specifying the commonalities and variabilities between the artifacts of the individual products. The number of products generated by a hierarchical model is exponential in its size, which poses a serious challenge to software product line analysis and verification. For an analysis technique to scale, the effort has to be linear in the size of the model rather than linear in the number of products it generates. Hence, efficient product line verification is only possible if a compositional verification technique allows the analysis of products to be relativized on the properties of their variation points. In this presentation, I show simple hierarchical variability models (SHVM) with explicit variation points as a way to describe a set of products consisting of sets of methods. SHVMs provide a trade–off between expressiveness and a clean and simple model suitable for compositional verification. We generalize a previously developed compositional technique and tool set for the automatic verification of control–flow based temporal safety properties to product lines defined by SHVMs.