Timing verification by successive approximation
First Claim
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.
8 Assignments
0 Petitions
Accused Products
Abstract
Apparatus for developing and verifying systems. The disclosed apparatus employs a computationally-tractable technique for verifying whether a system made up of a set of processes, each of which has at least one delay constraint associated with it, satisfies a given temporal property. The technique deals with the verification as a language inclusion problem, i.e., it represents both the set of processes and the temporal property as automata and determines whether there is a restriction of the set of processes such that the language of the automaton representing the restricted set of processes is included in the language of the automaton representing the temporal property. The technique is computationally tractable because it deals with the problem iteratively: it tests whether a current restriction of the set of processes is included, and if not, it employs a counter-example for the inclusion to either determine that the delay constraints render satisfaction of the given temporal property or to derive a new restriction of the set of processes. Further included in the disclosure are techniques for checking the timing consistency of the counter-example with respect to a delay constraint and techniques for finding the optimal delay constraint.
103 Citations
11 Claims
-
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. - View Dependent Claims (2)
-
-
3. Improved apparatus implemented in a computer system for generating a machine-executable implementation specification for a finite state machine of practical size, the apparatus including
refinement means for receiving a model of the finite state machine and refining the model and verification means for receiving the refined model and a task for the model which specifies a given temporal property and responding to the refined model and the task by verifying that the refined model can perform the task and the improvement comprising: timing verification means in the verification means for verifying that delay constraints in the refined model satisfy the given temporal property, the timing verification means remaining computationally tractable for the finite state machine. - View Dependent Claims (4, 5, 6)
-
7. A method used in apparatus for developing a finite state machine to develop a finite state machine of practical size comprising the steps performed in the apparatus for developing the finite state machine of:
-
receiving a model of the finite state machine; refining the model; and verifying that the refined model can perform a task which specifies a given temporal property, the step of verifying including the step of verifying for the finite state machine in a computationally tractable manner that delay constraints in the refined model satisfy the given temporal property. - View Dependent Claims (8, 9, 10)
-
-
11. Improved apparatus implemented in a computer system for generating a machine-executable implementation specification for a system from a logical definition of the implementation and a logical definition of the system'"'"'s behavior, the behavior including a given temporal property and the logical definition of the implementation specifying a set of processes with delay constraints, the apparatus including verification means for verifying that a system implemented according to the logical definition of the implementation will perform according to the logical definition of the system'"'"'s behavior, and the improvement comprising:
-
timing verification means in the verification means for verifying that the delay constraints satisfy the given temporal property by executing steps including 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.
-
Specification