Systematically deriving partial oracles for testing concurrent programs

The problem of verifying the correctness of test executions is well-known: while manual verification is time-consuming and error-prone, developing an oracle to automatically verify test executions can be as costly as implementing the original program. This is especially true for concurrent programs, due to their non-determinism and complexity. In this paper, we present a method that uses partial specifications to systematically derive oracles for concurrent programs. We illustrate the method by deriving an Ada task that monitors the execution of a concurrent Ada program and describe a prototype tool that partially automates the derivation process. We present the results of a study that shows the derived oracles are surprisingly effective at error detection. The study also shows that manual verification is an inaccurate means of failure detection, that large test case sets must be used to ensure adequate testing coverage, and that test cases must be run many times to cover for variations in run-time behaviour