Assertion-based Verification: From Compile-time Checking to Runtime Error Recovery

基于断言的验证：从编译时检查到运行时错误恢复isarfraz khurshidabstract该项目研究基于断言的修复——一种使软件系统在出现故障之前从错误中恢复的新方法。传统的错误恢复方法使用断言计算来检测错误状态，并使用专门的例程来修复它们。这些例程中的大多数都是临时的，难以理解的，并且无法处理各种错误。这个项目的关键见解是，通过使用断言作为执行修复的基础，将违反的断言转换为修复例程。这个项目将开发系统的方法，使使用通用编程语言（如Java）编写的断言能够进行有效的修复。修复方法将使用各种复杂的数据结构进行评估。提出的方法的实现为编译时检查和运行时错误恢复提供了一个统一的框架——这两种软件可靠性方法传统上部署了非常不同的算法。这种统一具有显著提高软件质量的潜力。任何带有断言注释的程序，程序员都可以轻松编写，可以：(1)在使用现有技术部署之前进行系统检查；(2)保证在使用建议的方法部署后继续执行，不会出现故障。

Proposal NumberCCF-0702680TITLEAssertion-based Verification: From Compile-time Checking to Runtime Error RecoveryPISarfraz KhurshidAbstractThis project investigates assertion-based repair---a novel methodology for enabling software systems to recover from errors before they manifest into failures. Traditional approaches to error recovery use assertion evaluations to detect erroneous states and specialized routines to repair them. Most of these routines are ad hoc, ill-understood, and unable to handle a variety of errors.The key insight of this project is to turn a violated assertion into a repair routine by using the assertion as a basis of performing repair. This project will develop systematic approaches that enable efficient repair using assertions written in common programming languages, such as Java. The repair approaches will be evaluated using a variety of complex data structures.Realization of the proposed methodology enables a unified framework for compile-time checking and runtime error recovery -- two software reliability methodologies that traditionally have deployed very different algorithms. The unification has the potential to significantly increase the quality of software. Any program that is annotated with assertions, which programmers already write comfortably, can be: (1) systematically checked before deployment using existing techniques; and (2) guaranteed to continue to execute without failure, once deployed, using the proposed methodology.