Collaborative Research: Compositional Verification of Software Product Lines as Open Systems

点击翻译按钮获取中文摘要

0305950Krishnamurthi, Shriram, -Brown UniversityCollaborative Research: Compositional Verification of Software ProductLines as Open Systems0305834Fisler, Kathryn, -Worcester Polytechnic InstituteCollaborative Research: Compositional Verification of Software ProductLines as Open SystemsA 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 demonstratedsoftware engineering benefits, they pose a nontrivial challenge for traditional methods of testing and validation. Prior work, including case studies, has developed compositional techniques for automatedverification 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 andacross 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 andexperimental validation. The project both contributes to advancing an important software development methodology and narrows the gap between the areas of software engineering and computer-aidedverification. The work involves undergraduate students and will have impact through classroom contact at several levels.