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.