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

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

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.