Krishnamurthi, Shriram, - Brown University Collaborative Research: Compositional Verification of Software Product Lines as Open Systems
0305834 Fisler, Kathryn, - Worcester Polytechnic Institute Collaborative Research: Compositional Verification of Software Product Lines as Open Systems
A product line is a family of related software products built from a common set of components, where each component typically implements a distinguishable feature. While product lines have many demonstrated software engineering benefits, they pose a nontrivial challenge for traditional methods of testing and validation. Prior work, including case studies, has developed compositional techniques for automated verification of temporal logic formulae over product lines. The case studies have revealed the need for techniques that handle open system verification sensitive to (a) propositions that evolve over time and across features, and (b) propositions that behave differently depending on whether they model control or data. This project, a collaboration between Brown University and Worcester Polytechnic Institute, extends prior work to handle these issues using a particular combination of propositional, temporal, and 3-valued logic constraints. The combined representations lead to lightweight preservation checks, a crucial part of keeping product-line verification tractable. The work includes both theoretical work and experimental validation. The project both contributes to advancing an important software development methodology and narrows the gap between the areas of software engineering and computer-aided verification. The work involves undergraduate students and will have impact through classroom contact at several levels.
