The Certification Trail Approach to Software Fault Tolerance and Testability

这项研究调查了一种技术，该技术允许构建更容易和更有效地测试的计算机程序，并且可以将其结合到设计方法中，以产生高效的可测试和容错的软件系统。这种技术是修改主应用程序，以便主程序不仅产生其所需的输出，而且还生成额外的数据，这种情况下的开销基本上可以忽略不计，这就是我们所说的“认证跟踪”。认证跟踪允许借助于第二个更简单且更有效地执行的程序来完全和有效地认证主程序的输出的正确性，该第二个更简单且更有效地执行的程序被称为“认证器”，它使用认证跟踪也产生输出，以便可以进行后续的比较操作。与执行速度相比，认证器的相对简单具有显著的优势。例如，在对主程序进行验证要复杂得多的情况下，可以正式地验证验证器程序的正确性-也许是令人望而却步。总体而言，该项目为认证跟踪技术开发了一个正式的理论框架，并通过实施该技术并为实现各种知名算法的主要程序生成性能数据来构建概念验证性能实验。

This research investigates a technique which allows computer programs to be constructed which are more easily and efficiently tested and which can be incorporated into a design methodology for producing efficiently testable and fault tolerant software systems. The technique is to modify a primary applications program so that, with essentially negligible overhead, the primary program not only produces its required output but also generates additional data, referred to as a ``certification trail.'' The certification trail allows the correctness of the primary program's output to be completely and efficiently certified by means of a second, simpler and more efficiently executed program, referred to as a ``certifier'' which uses the certification trail to also produce the output so that a subsequent comparison operation can take place. The relative simplicity of the certifier has significant advantages beyond that of speed of execution. For example, the certifier program can be formally verified for correctness in cases where doing so for the primary program is much more complicated --- perhaps prohibitively so. In general, this project develops a formal, theoritical framework for the certification trail technique, as well as for building upon proof-of-concept performance experimentation by means of implementing the technique and generating performance data for primary programs implementing a variety of well-known algorithms.