National Science Foundation CCR-9505392
Principal Investigator:
Laura K. Dillon
Computer Science Department
3115 Engineering Building
Michigan State University
East Lansing, MI 48826
Project Summary. 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 is investigating the use of oracles created from Graphical Interval Logic (GIL) specifications in testing and debugging of real-time programs. Existing technology should permit fairly rapid transfer of GIL-based oracles that automate the verification of executions in support of these essential validation activities.
GIL is a highly intuitive 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. The current project builds on a prior project on GIL. We are developing methods for relating GIL specifications to real-time programs that permit 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 can construct a GIL formula describing a fault in the execution. Displaying this formula graphically, appropriately aligned with an execution trace, helps 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 be an important facet of the project. The project combines analytical research on formal methods with experimental research aimed at assessing the practical utility of formal methods.