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

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

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.