Oracles for checking temporal properties of concurrent systems

1 December 1994

proceedings article
Published by Association for Computing Machinery (ACM)

Vol. 19 (5) , 140-153
https://doi.org/10.1145/193173.195401

Abstract

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 verification of test executions.This paper examines the use of Graphical Interval Logic (GIL) for specifying temporal properties of concurrent systems and describes a method for constructing oracles from GIL specifications. The visually intuitive representation of GIL specifications makes them easier to develop and to understand than specifications written in more traditional temporal logics.Additionally, when a test execution violates a GIL specification, the associated oracle provides information about a fault. This information can be displayed visually, together with the execution, to help the system developer see where in the execution a fault was detected and the nature of the fault.

Keywords

This publication has 11 references indexed in Scilit:

A graphical interval logic for specifying concurrent systems
ACM Transactions on Software Engineering and Methodology, 1994
TAOS: Testing with Analysis and Oracle Support
Published by Association for Computing Machinery (ACM) ,1994
State-based model checking of event-driven system requirements
IEEE Transactions on Software Engineering, 1993
Graphical specifications for concurrent software systems
Published by Association for Computing Machinery (ACM) ,1992
Specifying concurrent systems with TSL
IEEE Software, 1991
Real-time interval logic for reasoning about executions of real-time programs
ACM SIGSOFT Software Engineering Notes, 1989
Trace analysis for conformance and arbitration testing
IEEE Transactions on Software Engineering, 1989
Proceedings of the ACM SIGSOFT '89 third symposium on Software testing, analysis, and verification - TAV3
Published by Association for Computing Machinery (ACM) ,1989
Automatic verification of finite-state concurrent systems using temporal logic specifications
ACM Transactions on Programming Languages and Systems, 1986
An interval logic for higher-level temporal reasoning
Published by Association for Computing Machinery (ACM) ,1983