Abstract
Generating Oracles From Your Favorite Temporal Specifications
by: Laura K. Dillon and Y. S. Ramakrishna
Abstract:
The paper describes a generic tableau algorithm, which is the basis for ageneral customizable method for producing oracles from temporal logicspecifications. A generic argument gives semantic rules with which to buildthe semantic tableau for a specification. Parameterizing the tableau algorithmby semantic rules permits it to easily accommodate a variety of temporaloperators and provides a clean mechanism for fine-tuning the algorithm toproduce efficient oracles.The paper develops conditions that ensure a set of rules results in a correcttableau procedure. It gives sample rules for a variety of linear-time temporaloperators and shows how rules are tailored to reduce the size of an oracle. Toillustrate the versatility of this method, its application to a high levelinterval logic is discussed.
Keywords:
Formal specification and validation methods, Specification-basedtest oracles, Trace checking, Temporal logic, Concurrent systems
Date:
August 1995
Document: 1995-15
