Theory of Program Checking and Fault-Tolerant Software

程序检查与软件容错理论

• 批准号: 9315696
• 负责人: Michael Loui
• 金额: $ 11.65万
• 依托单位: University of Illinois at Urbana-Champaign
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1994
• 资助国家: 美国
• 起止时间: 1994-09-01 至 1997-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9315696&HistoricalAwards=false
• 关键词: Theory; Program; Checking; Fault; Tolerant

Program checking is a new approach to software fault-tolerance. For a program that computes a function, a checker tests whether the program's output is correct for a specific input. Even when the program makes mistakes, the checker uses the program itself to perform the test by applying the program to several inputs related to the original one. The checker provides a probabilistic guarantee of correctness on a particular input on which the program is executed, whereas formal program verification establishes correctness on all inputs prior to execution. In this project, traditional fault-tolerance techniques are combined with program checking to produce new kinds of program checkers that are effective for programs of practical size. In particular, program checking is combined with certification trails and with algorithm-based fault-tolerance, a technique for concurrent error detection. Further, program checking is applied to operating system algorithms that ensure the truth of predicates such as mutual exclusion, deadlock avoidance, and serializability of concurrent transactions.

程序检查是一种新的软件容错方法。 对于计算函数的程序，检查器会测试程序的输出对于特定输入是否正确。 即使程序出错，检查器也会使用程序本身来执行测试，方法是将程序应用于与原始输入相关的多个输入。 检查器为执行程序的特定输入提供正确性的概率保证，而形式程序验证则在执行之前确定所有输入的正确性。 在这个项目中，传统的容错技术与程序检查相结合，产生了对实际规模的程序有效的新型程序检查器。特别是，程序检查与认证跟踪和基于算法的容错（一种并发错误检测技术）相结合。 此外，程序检查应用于操作系统算法，以确保谓词的真实性，例如互斥、避免死锁和并发事务的可串行性。