Regression Verification in a User-Centered Software Development Process for Evolving Automated Production Systems

用于不断发展的自动化生产系统的以用户为中心的软件开发过程中的回归验证

• 批准号: 221572075
• 负责人: Professor Dr. Bernhard Beckert
• 金额: --
• 依托单位: Institut für Theoretische Informatik (ITI)
• 依托单位国家: 德国
• 项目类别: Priority Programmes
• 财政年份: 2012
• 资助国家: 德国
• 起止时间: 2011-12-31 至 2021-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/221572075?language=en
• 关键词: Regression; Verification; User; Centered; Software

The goal of this project is to leverage advances in deductive program verification to enable regression verification, i.e., proving formally that software remains correct through its evolution, and no new bugs are introduced. We aim to develop a regression verification methodology for a real object-oriented language (Java) that has the reach and power to be applied to real-world software. Even though building software with high quality from the beginning of the software lifecycle is crucial, it is not enough, since long-living software is adapted and evolves during its development and after its release. While traditional regression testing techniques are commonly used to give confidence in the reliability of evolving software, more powerful and reliable techniques are required. Over the last decade, there has been tremendous progress in the area of program verification. However, in the development of formal methods not enough attention has been given to software changes, which occur during software evolution. A very promising solution is to develop regression verification methods. They are a natural extension of regression testing. Given two programs that are both complex but similar to each other, much less effort is required to prove their equivalence than to prove that they satisfy a (complex) functional specification. The effort for proving equivalence mainly depends on the difference between the programs and not on their overall size and complexity. Our vision and goal is to develop regression verification methods powerful enough to be applicable to real-word software (and its evolution). We will develop regression verification methods for Java that can be used to prove that two Java programs are equivalent. We also address the problem of changing requirements by proving that two programs are not fully equivalent but differ in a formally specified way. We will implement these methods in a regression verification system based on our Java verification tool KeY. Regression verification shows its power (and only makes sense) as part of software evolution. It is central to the success of the proposed project that we integrate our methods into the software development and adaptation process. In particular, we plan to integrate regression verification with refactoring and reengineering of software, with software product line techniques, and with test generation and test selection. Our project thus addresses the priority programme’s guiding theme of methods and processes, contributing to the programme topics of (a) model-based and model-driven development of long-living systems, (b) traceability from requirements to architecture and code, and (c) continuous software system evolution under design (and to a lesser extent also runtime) control and management. We link to the application domains using case studies from the area of information systems, in particular the priority-programme-wide CoCoME case study.

该项目的目标是利用演绎程序验证的进步来实现回归验证，即，正式证明软件在其进化过程中保持正确，并且没有引入新的错误。我们的目标是开发一个回归验证方法的真实的面向对象的语言（Java），有能力应用到现实世界的软件。尽管从软件生命周期的一开始就构建高质量的软件是至关重要的，但这还不够，因为长寿的软件在其开发过程中和发布后都会适应和发展。虽然传统的回归测试技术通常用于对不断发展的软件的可靠性提供信心，但需要更强大和可靠的技术。在过去的十年里，在程序验证领域取得了巨大的进展。然而，在形式化方法的发展没有得到足够的重视，软件的变化，这发生在软件演化。一个非常有前途的解决方案是开发回归验证方法。它们是回归测试的自然延伸。给定两个程序都很复杂但彼此相似，证明它们的等价性比证明它们满足（复杂的）功能规范要少得多。证明等价性的努力主要取决于程序之间的差异，而不是它们的整体大小和复杂性。我们的愿景和目标是开发足够强大的回归验证方法，以适用于现实世界的软件（及其演变）。我们将为Java开发回归验证方法，可用于证明两个Java程序是等效的。我们还解决的问题，通过证明两个程序是不完全等同的，但在一个正式指定的方式不同的要求。我们将在一个基于Java验证工具KeY的回归验证系统中实现这些方法。回归验证作为软件演化的一部分显示了它的力量（并且只有有意义）。它是中央的成功，我们建议的项目，我们将我们的方法集成到软件开发和适应过程。特别是，我们计划将回归验证与软件重构和再工程、软件产品线技术以及测试生成和测试选择相结合。因此，我们的项目涉及优先方案的方法和过程指导主题，有助于（a）基于模型和模型驱动的长寿系统开发，（B）从需求到体系结构和代码的可追溯性，以及（c）在设计（以及在较小程度上还有运行时）控制和管理下的持续软件系统演变。我们使用信息系统领域的案例研究链接到应用领域，特别是优先级方案范围的CoCoME案例研究。