Directly verifying a black box system

Details Directly verifying a black box system Directly verifying a black box system

1999-09-14

2003-02-25

Smith, Matthew (Department: 2825)

Computer-aided design and analysis of circuits and semiconductor

Nanotechnology related integrated circuit design

C716S030000

Reexamination Certificate

active

06526544

ABSTRACT:

FIELD OF THE INVENTION
This invention relates generally to system verification and more particularly to verification of black box systems.
BACKGROUND
Model checking is a collection of methods for checking the reliability of a system design. In model checking, a description of the system, typically some finite state machine description, is checked for some property, such as mutual exclusion or responsiveness. In automata-based model checking, the complement of the property of interest and the system or system feature of interest are represented as automata. If there is an accepting run in the complement of the property automaton that is executable by the system automaton, then the system exhibits a counterexample of the desired property.
Model checking, therefore, indirectly checks whether a system exhibits some behavior. Since model checking is not applied to an actual system, the check is only as good as the system model. If the model contains errors, verifying that the model exhibits some property will not necessarily verify that the system exhibits the property.
Testing, on the other hand, is usually applied to the actual system (also called the implementation), rather than a description of the system, and checks whether the implementation conforms to the design. The test engineer applies a sequence of inputs to the implementation and observes the behavior of the system in relation to the inputs. From these behaviors, it is determined whether the implementation conforms to a design model. Conformance testing, unlike model checking, is not typically used for checking whether the implementation satisfies some property, and these techniques will not check an implementation directly for a property.
It is also a disadvantage of known system verification techniques that model checking requires knowledge of the internal structure of the system. For example, the finite state machines commonly used in model checking reveal the system's states and state transitions. Without knowledge of this structure, model checking becomes impractical. In real world system design, however, the internal structure is not always available, particularly when the system has evolved through many revisions. In cases of black box systems, there are no satisfactory methods for directly determining whether the black box exhibits some property. A black box system is a finite state system where the states and state transitions are unknown. Such systems are said to have unknown internal structure.
There are limited techniques for identifying a state machine for a black box by inferring the structure of the black box system. For instance, if two machines with n states are not equivalent, then there is at least one input string with a maximum length of 2n−1 characters that distinguishes the machines. In other words, any machine with n states is characterized by its output for all input strings of length 2n −1 characters, and a black box is uniquely determined by applying all such input strings. To infer the structure, a tree of depth 2n −1 is constructed from the responses of the black box to the input string. The tree is minimized to produce a minimal machine consistent with these outputs. This approach is explained in B. A. Trakhtenbrot, Y. M. Barzdin,
Finite Automata: Behavior and Synthesis,
North Holland, 1973. Known model checking can then be used to check whether the machine satisfies some property.
The known methods for inferring a machine and then applying model checking are computationally inefficient and have not received widespread use. One disadvantage is that these techniques cannot be used until the entire machine is inferred. If the property could be checked without knowledge of all the structure, these resources are wasted. Furthermore, known black box techniques do not provide for on-the-fly conformance testing between the black box and the inferred model. A method that permits on-the-fly model checking directly on the black box and also provides for construction of a minimal model would greatly improve system design efficiency. The need remains, therefore, for a method for efficiently and directly checking that a system satisfies certain properties where the design and internal structure of the system are largely unknown, for constructing a model of such a system, and for verifying that the model conforms to the black box.
SUMMARY
A system and method according to the principles of the invention provides for efficient and direct black box system checking. A black box system (hereafter alternatively referred to as black box or black box system) is a finite state system where the states and state transitions are unknown. For any property, a sequence of inputs for the black box is determined that will verify that the system exhibits the property. Counterexamples of the property are detected without inferring the black box's internal structure; that is, the model-check proceeds without identifying all states and state transitions of the black box. An exemplary method includes constructing a specification automaton operable to exhibit undesirable system behavior and configuring a black box as an automaton. It is then determined whether an accepting execution exists on the intersection of the black box automaton and the specification automaton.
For a deterministic system having an upper bound of n states and where the permissible inputs to the system are known, the system can be checked for a property through experiments on the black box. An experiment is an application of an input or string of inputs to the black box. To run the experiments, the black box is configured such that it can be reset to its initial state upon command and such that the system indicates when an input is disabled from a current state. When an input is enabled, the implementation transitions to the next state. If an input is disabled, then there is no intersection on the input string. The inputs are determined through a search of a specification automaton for accepting sequences up to a given bound. The bound is the product of the number of states of the black box and the specification automaton.
The specification automaton is configured as a finite automaton on infinite words, such as a Büchi automaton. Its alphabet is included in the alphabet of the black box automaton. The specification automaton is searched for an accepting run. A run is accepting if the automaton has a prefix, &sgr;
1
, starting from an initial state and terminating in an accepting state followed by a cycle, &sgr;
2
, that begins with and terminates in the same accepting state. The experiments include inputting &sgr;
1
&sgr;
2
to the black box. There is an accepting execution on the intersection of the specification automaton and the black box, if, after the black box is reset to its initial state, the black box can execute &sgr;
1
followed by &sgr;
2
(n+1) times. In other words, if the black box is a three state system, there is an accepting execution on the intersection if the black box can execute the inputs of &sgr;
1
followed by the inputs of &sgr;
2
four times. If the intersection is empty, the specification automaton searches for another &sgr;
1
&sgr;
2
and continues the check until the upper bound for &sgr;
1
or &sgr;
2
is reached.
&sgr;
1
and &sgr;
2
can also be used to generate a model of the black box. To do so, a conjectured model is model-checked with respect to the specification automaton. If the conjectured model exhibits the behavior described by the specification automaton, &sgr;
1
and &sgr;
2
are input to the black box. A successful run over the strings indicates that the black box also exhibits the undesired behavior. The strings are then used as a counterexample for generating another conjectured model with more states. If the conjectured model does not exhibit the behavior of the specification automaton, conformance testing determines whether the conjectured model conforms to the black box. Where the conformance test fails, the strings are used as the counterexample for generating another

Affiliated with

Also associated with

Rating

Directly verifying a black box system does not yet have a rating. At this time, there are no reviews or comments for this patent.

If you have personal experience with Directly verifying a black box system, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Directly verifying a black box system will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFUS-PAI-O-3158663