Patent Document ID: 5483470
Application ID: 07906082
Patent Flag: 1

Claim One:
1. An improved method performed in a computer system for generating a machine-executable implementation specification for a system from a logical definition of an implementation of the system and a logical definition of the system's behaviour the logical definition of the system's behavior including a given temporal property and the logical definition of the implementation specifying a set of processes, each of which has delay constraint, the method including a step of verifying that the system will satisfy the logical definition of the system's behavior and the improvement comprising the steps practiced in the the step of verifying of: determining whether a test set of processes derived initially from the set of processes satisfies the given temporal property, and if the test set does, returning an indication that the system satisfies the given temporal property and terminating the method; and otherwise providing a counter example of a sequence of behaviors of the processes of the test set which does not satisfy the given temporal property; determining whether the counter example is timing consistent with the delay constraints and if the counter example is timing consistent, returning an indication that the system cannot satisfy the given temporal property and terminating the method; and employing the counter example to restrict the test set of processes and repeating the steps of the method with the restricted test set as the test set.