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.