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.
