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.