Error detection/correction and fault detection/recovery – Data processing system error or fault handling – Reliability and availability
Reexamination Certificate
2000-12-26
2004-03-30
Iqbal, Nadeem (Department: 2184)
Error detection/correction and fault detection/recovery
Data processing system error or fault handling
Reliability and availability
C703S002000
Reexamination Certificate
active
06715107
ABSTRACT:
FIELD OF THE INVENTION
This invention relates in general to model checking and, in particular, to model reduction techniques embedded in computer-implemented model checking.
REFERENCES
—Ilan Beer, Shoham Ben-David, Avner Landver—“
On
-
The
-
Fly Model Checking of RCTL Formulas
”, Computer Aided Verification, CAV '98, LNCS 1427 Canada, 1998.
—Edmund M Clarke, Orna Grumberg, Doron Peled—“
Model Checking
”, The MIT Press, Cambridge, Massachusetts London England, 1999 pp. 1-11.
—Hopcroft John E, Ullrnan Jeffrey D—“
Introduction to Automata Theory, Languages and Computations
”, Addison Wesley, New York, 1979.
—Matt Kaufmann, Andrew Martin, Carl Pixley—“
Design Constraints in Symbolic Model Checking
”, CAV '98, LNCS 1427 Canada, 1998.
—Kenneth L. McMillan—“
Symbolic Model Checking
”, Kluwer Academic Publishers, Massachusetts, 1993.
BACKGROUND OF THE INVENTION
When designing systems that can be modeled as Finite State Machines, tools are used to check the correctness of the final design with respect to a design specification before proceeding to mass-production. A formal verfication tool is usually a computer program which requires as input a mathematical model of the system and a specification of desired design criteria. Thus, for example, in an integrated circuit including combinatorial gates and memory elements the circuit may generate an acknowledge signal (ACK) in response to a request signal (REQ) and the design specification may require that the REQ signal will be followed by the ACK signal within three clock cycles.
From a knowledge of the design specification and the mathematical model of the integrated circuit, a computer program can determine whether the model meets the specified design criteria. In the “temporal logic model checking” approach for formal verification, specifications are usually expressed in a propositional temporal logic, and circuit designs and protocols are modeled as state-transitions systems. An efficient search procedure is then used to determine if the specification holds on the state-transition system. In other words, a computer program checks whether the state-transition system is a model for the specification [CGP].
This approach suffers from the state-explosion problem. That is, the size of the state-space of the model is exponential in the number of its state-variables. Since the search procedure explores the state-space, its complexity is exponential in the number of state-variables as well. Thus the size of the designs which can be verified by model checking, using given computer resources such as memory and processing capacity, is severely limited.
Hence automated means to reduce the state-space are extremely important for making the technique of model checking tractable for industrial size designs.
A reduction is a procedure that reduces the state-space, while preserving anti-validity of the formula (i.e. if a propositional temporal logic formula is not valid in the reduced model it is also not valid in the original model). Naturally, the more the reduction can cut off the state-space, the better its merit will be. A natural way to reduce the state-space is to limit the behaviors of the environment. Since the model is comprised of the design under verification and its environment, reduction of the state space can be achieved by way of restricting the environment.
One traditionally used method for writing environment models is describing them via a Finite State Machine (FSM). Another way, used by Carl Pixley [KMP] is to specify environment models as a collection of Boolean constraints. In this approach, all inputs of the design under test are left free, but in the course of reachability analysis the model-checker discards all states that violate any of the user-specified Boolean constraints.
Other tools [FormalCheck(TM), CVE(TM)] enable the user to describe models via temporal constraints.
This invention introduces an innovative way to describe models (and in particular environment models), using regular expressions.
TABLE I
Definitions
Computation-tree
a representation of all possible
executions of some finite-state machine
in a form of an infinite tree. A branch
in the tree corresponds to a specific
execution path starting at the initial
state (which is represented by the root
of the tree).
Depth of a state
The minimal number of iterations
required to explore the state, starting
at the initial set of states.
Design Under
the hardware design to be verified.
Verification
Environment
a description of the possible legal
behaviors of the input pins of the
design under verification possibly
represented by a state-transition
system.
Formula
a property of the design under
verification written in RCTL [BBL].
Language
the set of strings defined by a regular
of a Regular
expression.
Expression
Model
the design under verification plus its
environment.
Model checking
a method of formal verification [CGP].
RCTL
a logic used for specifying properties
of the design under verification [BBL].
Regular
an expression constructed by inductive
Expression
application of the operations ‘concate-
nation’, ‘or’ and ‘Kleene closure’ on a
set of Boolean expressions [HU].
Rule
a model and a set of formulas claiming
some properties regarding the model.
State
a valuation of all state-variables.
State variable
the model checker's representation of a
memory element.
State-space
the set of all possible states.
Symbolic model
a method of model checking which
checking
partially solves the state explosion
problem [CGP].
THE PROBLEM
It is therefore straightforward that the user desires a reduction, which removes all paths that do not lead to any of the behaviors he aims at verifying. Intuitively, the user would wish to guide the search to error-prone areas of the design, while completely disregarding the rest. However, with the existing methods for model description, mainly by deployment of finite state machines (FSMs), the user might find it difficult to manipulate the model in such a manner so that scenarios of interest, and only scenarios of interest, occur.
Loosely speaking, it would be desirable to give the user the ability to describe, with minimum effort (specifically without the need for FSM implementation), a restricted model, in which the state-space includes only paths specified by her to be of interest. Such a reduced state space model would be amenable to analysis using a smaller memory than the complete state-space model and would be analyzed more quickly for a given computer processing capacity.
SUMMARY OF THE INVENTION
It is thus an object of the invention to restrict the computaion-tree to include only model behaviors described by the user (via the regular expression) as interesting.
This object is realized in accordance with a first aspect of the invention by a computer-implemented method for pruning a computation-tree defining a set of model behaviors of a state machine to a subset of the model behaviors, thereby reducing a size of the computation-tree and allowing analysis thereof by a computer in a shorter calculation time than would be possible for the complete computation-tree, said method comprising the steps of:
(a) obtaining as input:
i) a mathematical model of a Finite State Machine, and
ii) a Regular Expression defining a set of behaviors that are of interest to the user,
(b) using the Regular Expression to construct:
i) a finite automaton accepting all prefixes of words accepted by the Regular Expression, and
ii) a Boolean expression that realizes a property that the state is part of some path of a behavior defined by the Regular Expression, i.e. the expression evaluates to a first logic symbol for each of said words that are defined by the Regular Expression and evaluates to a second logic symbol otherwise, and
(c) exploring a state space of a product machine comprising the Finite State Machine and the constructed finite automaton such that for each state of the product machine there exists a corresponding Finite State Machine component and a correspondin
Beer Ilan
Fisman Dana
Gluhovsky Leonid
Yatzhar-Haham Tali
International Business Machines - Corporation
Iqbal Nadeem
LandOfFree
Method and system for reducing the computation tree to... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Method and system for reducing the computation tree to..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method and system for reducing the computation tree to... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3208891