Patent ID: 7149987

Claim:
A method for verifying whether a trace can be produced by a generator, comprising: receiving a specification for the generator, wherein the generator is a finite state machine that defines a set of inputs and outputs, and wherein the generator contains parametric inputs to model non-determinism; receiving the trace, wherein the trace is a sequence of assignments of non-parametric inputs and outputs for the generator, and wherein the trace does not contain assignments of parametric inputs; using the specification to build a data structure that can be used to determine if a non-parametric input and output are consistent with the current state of the generator; verifying elements of the trace, wherein verifying a given element involves using the data structure to determine if there exists any parametric input assignment that causes a match between non-parametric inputs and outputs of the generator with the ones specified in the given element of the trace; and if the specification of the generator is sequentially deterministic, and hence does not depend on parametric inputs, translating the generator into a checker and using that checker to verify the trace.