Abstract Generating Oracles from Your Favorite Temporal Logic Specifications.pdf

Generating Oracles from Your Favorite Temporal Logic Specifications* L. K. Dillon Y. S. Ramakrishna Computer Science Department Computer Science Department University of California State University of New York Santa Barbara, CA 93106 Stony Brook, NY 11794 Abstract This paper describes a generic tableau algorithm, which is the basis for a general customizable method for producing oracles from temporal logic specifications. A generic argu- ment gives semantic rules with which to build the semantic tableau for a specification. Parameterizing the tableau al- gorithm by semantic rules permits it to easily accommodate a variety of temporal operators and provides a clean mech- anism for fine-tuning the algorithm to produce efficient or- acles. The paper develops conditions to ensure that a set of rules results in a correct tableau procedure. It gives sam- ple rules for a variety of linear-time temporal operators and shows how rules are tailored to reduce the size of an oracle. Keywords: formal specification, verification, specification- based test oracles, tableau methods, propositional temporal logic, test vdldation. 1 Introduction Temporal specifications describe constraints on the order in which events can occur in executions of a concurrent soft- ware system. Oracles produced from these specifications can verify that traces generated by executing a system conform to the specifications. Such oracles are needed during system testing to uncover temporal faults in test executions [16]. Proactive debuggers and run-time monitors can use tempo- ral oracles to detect faults, notifying the user when they occur [8]. If efficient, temporal oracles can also be incorpo- rated into robust, self-checking programs [1]. Several methods for checking that traces conform to tem- poral specifications have been designed for specific nota- tions [2, 4, 12, 13]. The precise semantics of the operators that a notation provides motivate details of the methods. This practice makes it difficult to