Abstract Oracles for Checking Temporal Properties of Concurrent Systems

Verifying that test executions are correct is a crucial step in the testing process. Unfortunately, it can be a very arduous and error-prone step, especially when testing a concurrent system. System developers can therefore benefit from oracles automating the verifi-cation of test executions. This paper examines the use of Graphical Interval Logic (GIL) for specifying temporal properties of con-current systems and describes a method for construct-ing oracles from GIL specifications. The visually intuitive representation of GIL specifications makes them easier to develop and to understand than spec-ifications written in more traditional temporal logics. Additionally, when a test execution violates a GIL specification, the associated oracle provides informa-tion about a fault. This information can be displayed visually, together with the execution, to help the sys-tem developer see where in the execution a fault was detected and the nature of the fault.