Automated Support for Testing and Debugging of Real-Time Programs Using Oracles

当今软件工程师面临的巨大挑战之一是开发可靠的系统，这些系统在所有情况下都能正确运行。最关键的应用程序通常涉及并发性和实时性，这增加了系统开发和验证的难度。测试和调试不能证明系统是正确的。然而，它们是目前验证实际应用程序最有效的方法。这个项目研究了在实时程序的测试和调试中使用图形间隔逻辑（GIL）规范创建的oracle。GIL是一种用于指定和推理实时系统属性的可视化逻辑。现有的GIL工具允许机械地检查系统规范是否保证了关键的正确性需求。该项目旨在产生一种将GIL规范与实时程序联系起来的方法，该方法允许使用由GIL规范构建的确定性有限状态自动机来验证程序的执行是否正确。当执行违反规范时，相关的oracle将构造一个GIL公式来描述执行中的错误。该公式将以图形方式显示，并与执行跟踪适当对齐，以帮助用户查看跟踪中的错误发生位置和错误的性质。如果软件工程师要在实际系统的开发中使用形式化方法，那么形式化方法必须是自动化的。因此，原型的实施和实验评估是该项目的一个重要方面，该项目将形式方法的分析研究与旨在评估形式方法实际效用的实验研究相结合。

One of the great challenges facing today's software engineers is the development of reliable systems, which are known to perform correctly in all circumstances. The most critical applications often involve concurrency and real-time, which increase the difficulty of system development and validation. Testing and debugging cannot prove a system is correct. However, they are currently the most effective methods available for validating real applications. This project investigates the use of oracles created from Graphical Interval Logic (GIL) specifications in testing and debugging of real-time programs. GIL is a visual logic for specifying and reasoning about properties of real-time systems. The existing GIL tools allow mechanical checking that system specifications guarantee critical correctness requirements. This project seeks to produce a method for relating GIL specifications to real-time programs that permits deterministic finite-state automata constructed from GIL specifications to be used in verifying that executions of a program are correct. When an execution violates a specification, the associated oracle would construct a GIL formula describing a fault in the execution. This formula would be displayed graphically, appropriately aligned with an execution trace, to help the user see where in the trace the fault occurred and the nature of the fault. Formal methods must be automated if software engineers are to use them in the development of real systems. The implementation and experimental evaluation of prototypes is therefore an important facet of this project, which combines analytical research on formal methods with experimental research aimed at assessing the practical utility of formal methods.