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

0305950Krishnamurthi，Shriram，-Brown University合作研究：作为开放系统的软件产品线的组合验证Fisler，Kathryn，-Worcester理工学院合作研究：作为开放系统的软件产品线的组合验证产品线是由一组公共组件构建的相关软件产品系列，其中每个组件通常实现一个可区分的功能。虽然产品线有许多已被证明的软件工程好处，但它们对传统的测试和验证方法构成了不小的挑战。以前的工作，包括案例研究，已经开发出组合技术，用于自动验证产品线上的时态逻辑公式。案例研究表明，需要处理开放系统验证的技术，这些技术对(A)随时间和跨特征演变的命题以及(B)行为不同的命题(取决于它们是模拟控制还是数据)敏感。这个项目是布朗大学和伍斯特理工学院的合作项目，扩展了以前的工作，使用命题、时间和三值逻辑约束的特定组合来处理这些问题。组合的表示导致了轻量级的保存检查，这是保持产品线验证容易处理的关键部分。这项工作包括理论工作和实验验证。该项目既有助于推进一种重要的软件开发方法，又缩小了软件工程领域和计算机辅助核查领域之间的差距。这项工作涉及本科生，并将通过课堂接触在几个层面上产生影响。

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.