Detecting of model errors through simplification of model...

Details Detecting of model errors through simplification of model... Detecting of model errors through simplification of model...

1998-12-14

2001-10-30

Beausoleil, Robert (Department: 2184)

Error detection/correction and fault detection/recovery

Data processing system error or fault handling

Reliability and availability

C716S030000, C703S013000

Reexamination Certificate

active

06311293

ABSTRACT:

FIELD OF THE INVENTION
The present invention relates to system verification, and more particularly to a method and apparatus for checking the behavior of finite state system models.
BACKGROUND OF THE INVENTION
An ongoing problem in the design of large systems is verifying that the system will behave in the manner intended by its designers. One approach has been to simply build and test the system itself. Of course, building a system can be an expensive proposition and, therefore, artisans have migrated toward building and testing a model of the system through software.
In a software environment, a system model is typically embodied in a block of code that, when executed, simulates the intended functions and/or features (properties) of the system. More specifically, the system model accepts inputs, performs functions and (generates outputs in the same manner as would the actual system. By controlling the value of the system model inputs and monitoring the system model outputs, the functionality, or properties, of the system can be thus tested.
One method of testing a system model is called formal verification. In formal verification, the system model is fed into a verification tool that converts the system model into a finite state machine. The finite state machine is a set of states and state transitions that mimic the operation of the system model in response to any given set of system model inputs. More specifically, each state represents a state of the system, and each state transition indicates the conditions (i.e., the values of external inputs and system variables) that must be met for the system to transition from one state to another state.
Once a system model is converted to a state machine, the verification tests whether the system model behaves according to a set of expected behaviors. To do this, the verification tool varies the system model inputs and monitors which states the system model enters as a result of the inputs. This has been referred to as searching the state space of the system model. While searching the system model state space, the verification tool can check whether the system model enters a state or a cycle of states which the designers of the system define as “bad” or unintended. If the system model enters a “bad” state or a “bad” cycle of states, the system model is said to behave in a manner contradictory to that intended by the system designer, thus requiring a redesign.
Viewed more formally, it is said that a system has two classes of properties: safety and liveness. A safety property violation is a violation that can be detected in the course of performing the reachability analysis, because it relates to conditions that may be falsified at a given state. For example, given a condition such as x is always equal to y defines a safety property whose correctness can be checked in the course of determining the reachable states. A liveness property is one which can be falsified at some state in the course of a reachability analysis. An example of such a property is “if request x, eventually grant y”. A proof of a failure of a liveness property may take an infinite sequence because, as can be readily observed from the above example, in any finite number of steps (that don't end up in a cycle) the next step might satisfy the property (y would be granted). Another way to describe a safety property is one where “nothing bad will happen”. A liveness property is one where “something good will (eventually) happen”.
Heretofore, to fully test every property of the system model through formal verification, the verification tool has had to run a full search of the system model's reachable states from a designated set of initial states. A full search of a system model state space is a test wherein, at each state, the system model inputs are varied, and non-deterministic choices for the next state are varied, such that they take on every value they can possibly assume in every possible order or sequence. As a result, a full search of reachable states insures that the system model behavior is tested under every set of conditions that the system model can possibly undergo when in operation.
One can easily realize as the number of system model inputs increases, and as the range of assumable values for each input increases, the greater is the number of states of the system, and the greater the amount of computational resources that are necessary to complete a full search. In fact, it has been found that fully searching a reasonably complex models with conventional verification tools can cause the verification tool to run out of computational resources, such as memory to store temporary data. When this happens, the verification tool may “lock-up” without providing the tester with data as to whether the system model had behaved as expected and hoped.
One solution to this problem is to reduce the size of the system model and run a full search of the reduced model. That is, a tester who is experienced in the details of the system model eliminates portions of the system that the tester believes have no effect on the tested set of system properties, and proceeds with the reduces system model, hoping that the assumptions made were not erroneous. This may require, however, substantial time, effort and experience on the part of the tester to insure that the system model is not reduced so much as to fail to retain those portions that are critical for evaluating the tested properties. In addition, although reducing the system model reduces the amount of computational resources required to check the system model, such a reduction prevents a full search from checking the behavior of all system model properties.
Another solution to the computational resource problem associated with fully testing complex models is to perform only a partial search of the system model. A partial search is a test that identifies the states that the system model can enter when given a partial set of input values that are applied in a limited number of possible sequences. That is, a partial search does not test the behavior of the system model in response to every possible input value and in every possible sequence, as described above for the full search. Rather, during a partial search, the behavior of the system model is tested in response to only a portion of the total number of possible inputs.
Of course, the ability to identify design errors through a partial search is limited by the ability of the tester to predetermine which set of inputs may cause the system model to enter a “bad” state or cycle of states, as described above. This suggests that in order for the partial search to identify system model errors, the tester must either have intimate knowledge of the system model design, or be lucky enough to input a set of inputs in a sequence that exposes a “bad” or unintended system model behavior. Thus, by undertaking to perform a partial search to test a complex system model, the tester is left with the difficult task of guessing, which set of input values should be included in the partial search, and in what sequence the values should be input. This makes the task of checking the behavior of all system properties, or functions, substantially more difficult. Thus, such a partial search may not be a practical solution for testing a system model in many applications.
In a copending application, Ser. No. 09/923,297, filed Sep. 4, 1997, now U.S. Pat. No. 5,946,481, issued Aug. 31, 1999, an improved approach is disclosed. In this application, the system model is restricted based on the behavior of the system model during a partial search. A partial search is conducted in a prescribed manner, such as in accordance with a selected random process and, once the process terminates, the values assumed by system model variables or system model inputs during the partial search are used to restrict the set of assumable values for that variable or input. The restricted set of assumable values defines the values that the particular input or variable can assume during system model verification. Thus

Affiliated with

Also associated with

Rating

Detecting of model errors through simplification of model... does not yet have a rating. At this time, there are no reviews or comments for this patent.

If you have personal experience with Detecting of model errors through simplification of model..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Detecting of model errors through simplification of model... will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFUS-PAI-O-2606526