Data processing: structural design – modeling – simulation – and em – Modeling by mathematical expression
Reexamination Certificate
1997-10-07
2001-02-06
Teska, Kevin J. (Department: 2763)
Data processing: structural design, modeling, simulation, and em
Modeling by mathematical expression
C703S014000, C703S015000, C716S030000, C716S030000, C716S030000
Reexamination Certificate
active
06185516
ABSTRACT:
BACKGROUND OF THE INVENTION
1. Field of the Invention
The invention relates generally to determining whether a system will perform a given task correctly and more specifically to employing formal verification to make that determination.
2. Description of the Prior Art
A perennial problem in the design of large systems is verifying that the system will indeed behave in the manner intended by its designers. One approach has been simply to try out the system, either by building and testing the system itself or by building and testing a model of it. In recent years, this approach has taken the form of a computer simulation of the system. A computer program which is a model of the system is written, and the system is tested by executing the computer program. A fundamental problem with the approach of “trying out the system” is that the system's designers can only try out behavior which they anticipate. For any but the simplest systems, however, the designers cannot anticipate all of the behavior of the system, and it is of course always unanticipated behavior which causes difficulties.
As the limitations of simulation have become more apparent, interest has grown in the formal verification of system behavior. In formal verification, the designer provides a logical definition of the system's intended behavior and a logical definition of the implementation to a formal verification system. The formal verification system then determines whether the logical definition of the system's intended behavior implies the logical definition of the implementation. If it does, the implementation is faithful to the logical definition of the intended behavior.
A particularly useful kind of formal verification is automata-theoretic verification. In this type of formal verification, the system and the desired behavior are both modelled using a particular kind of finite state machine termed an automaton. A finite state machine consists of a set of states and a set of transitions between the states. A transition from one state to another takes place when a set of variables take on values which are required for the transition to occur. For example, an electrical circuit with a light bulb and a switch can be modelled as a finite state machine with two states light on and light off and a variable switch which has the value 0 when the switch is off and the value 1 when the switch is on. Transitions between the states take place when the value of switch changes. The initial state is light off; the finite state machine remains in the state until switch takes on the value 1. At that point, the finite state machine makes the transition to the light on state and remains in that state until switch takes on the value 0, whereupon the finite state machine makes the transition to the light off state.
One way of looking at the behavior of a finite state machine is to see it as responding to a sequence of values of the variables. For instance, the example finite state machine has only one variable, and that variable can have only two values, 0 and 1, so the example finite state machine will respond to any sequence of 0;0;1;0; and so forth. If there were two variables (for example, if the circuit had two switches), the finite state machine would respond to sequences of pairs of values, for example, 0,0; 0,1; and so forth.
An automaton is a finite state machine in which certain states are to be defined as final states. If an automaton is in one of the final states after it has received a sequence of values, the automaton is said to have accepted the sequence of values. In our example finite state machine, either of the two states is a final state, and the finite state machine is consequently an automaton which will accept any sequence of 0's and 1's.
In mathematical terms, the set of the sequences of values which an automaton accepts defines a language for the automaton. This is important for formal verification because when a system and a task are modelled as automata, the languages of the system and the task can be used to determine whether the system will perform the task. If the language defined by the automaton modelling the system is contained in the language defined by the automaton modelling the task, the system will perform the task. Otherwise, it will not.
The main problem with automata-theoretic verification is that the number of states and transitions in a system of finite state automata which represents a system of any size is so great that the state graphs which the programs that do automata-theoretic verification employ to represent the states of the system may exceed the storage capacity of the computer systems running the programs. Indeed, even if storage could be provided, the number of states is often so large that a computer system still would not be able to do the verification in a reasonable amount of time. This problem is termed the state-space explosion problem or more generally, the computational complexity problem.
The parents of the present patent application all disclose techniques for overcoming the computational complexity problem. One set of these techniques involves stepwise refinement of the system model from a simple model which can be verified to have desired properties to a model which has the complexity required for the actual implementation of the system and which can be verified to have inherited the desirable properties from the simple model. The techniques for stepwise refinement disclosed in the parent patent applications include the use of language homomorphisms to map behaviors of more detailed models into behaviors of less detailed models. As long as there is such a mapping, the behaviors of the more-detailed models preserve the properties of the behaviors of the less-detailed models.
Another set of the techniques involves reduction of the language containment test to a set of language containment tests which are together computationally less expensive than the original language containment test. The user of the verification system does a reduction by first decomposing the property that is being verified into local properties which, when taken together, imply the property being verified. The verification system verifies this implication. Then, the verification system “localizes” the system being verified with regard to each of the local properties. It does this by taking advantage of the fact that only a small part of the system being verified is concerned with the local property. Consequently, the rest of the system may be “abstracted away”, and the verification need be done only on the part which is concerned with the local property. If the verification succeeds for all of the local properties, then the property has been verified for the entire system.
A more detailed discussion of the foregoing techniques for dealing with the computational complexity problem and an example may be found at columns 17 through 70 of “Verification of Homomorphism Between Two System Models,” U.S. Pat. No. 5,740,084 issued Apr. 14, 1998, which is incorporated herein by reference. A description of a verification system which employs the stepwise refinement and reduction techniques described above may be found in Zvi Har'El et al., “Analytical Development and Verification of Control-intensive Finite State Machines,” U.S. Pat. No. 5,163,016, issued Nov. 10, 1992. That patent is hereby incorporated into the present patent application by reference.
The use of stepwise refinement and reduction in the system of U.S. Pat. No. 5,136,016 represented a major step in dealing with the problem complexity. Automata-theoretic verification however remains an expensive undertaking in terms of both computation time and memory resources. It is an object of the present invention to provide improved techniques for stepwise refinement and reduction which further reduce the cost of automata-theoretic verification.
SUMMARY OF THE INVENTION
The object of the present invention is attained by means of two techniques for reducing the size of the model automata used to test language containment
Hardin Ronald H.
Kurshan Robert Paul
DiGiorgio James
Lucent Technologies - Inc.
Sergent Douglas W.
Teska Kevin J.
LandOfFree
Automata-theoretic verification of systems does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Automata-theoretic verification of systems, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Automata-theoretic verification of systems will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2615222