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

0305950 Krishnamurthi，Shriram，-Brown University协作研究：开放系统软件产品线的组成验证0305834 Fisler，Kathryn，-Worcester Polytechnic InstituteCollaborative Research：开放系统软件产品线的组成验证产品线是由一组公共组件构建的相关软件产品系列，其中每个组件通常实现可区分的功能。 虽然产品线有许多证明软件工程的好处，他们提出了一个不平凡的挑战，传统的测试和验证方法。 以前的工作，包括案例研究，已经开发出的组成技术，自动验证的时间逻辑公式的产品线。 案例研究表明，需要处理开放系统验证敏感的技术（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.