Breadth-Bounded Model Checking
| Attachment | Size |
|---|---|
| BBMC.pdf | 237.36 KB |
Model checking large concurrent systems is a difficult task,
due to the infamous state space explosion problem. To combat this prob-
lem, a technique called Bounded Model Checking has been proposed.
This techniques relies on restricting the level of unfoldings of the tran-
sition relation of a given specification. This technique is quite effective
for verifying requirements that are relatively close to the initial state
of the system’s behaviour. Unfortunately, this technique is not adequate
for disproving requirements which occur at levels that are relatively deep
within the system. In this paper, we study an alternative approach to
BMC by restricting the breadth of the transition relation, based on a
Highway simulation. This allows us to find violations to (1) properties
that lurk deep in a specification, and (2) properties that require lengthy
counterexamples. Our experiments show that the method is complemen-
tary to BMC, and is effective in many practical applications.
Designing software for devices is a complex and challenging task. Analysing
designs prior to actually implementing these is good practice, though still not
very commonplace. Model checking is a popular technique for analysing designs,
and the functioning of a device as a whole. This technique essentially relies
on an exhaustive exploration of the system’s behaviour; it uses temporal logic
for formalising requirements on the system’s behaviour. Model checking can be
used to prove that requirements hold, or show that they are violated. However,
traditional model checking often suffers from the infamous state space explosion,
rendering the technique useless.
Various authors have proposed techniques to combat the state space explo-
sion, based on partial explorations of the state space. A notable example is the
technique of Bounded Model Checking (BMC), pioneered by Biere et al [4, 6].
This technique has been demonstrated to be quite effective in the verification of
industrial designs. Even though BMC is incomplete (it does not guarantee a true
or false determination for all specifications [6]), it has been used to find bugs in
situations where more traditional verification techniques fail completely. Being
incomplete still allows BMC to be used effectively for bug-hunting, i.e., finding
counterexamples to conjectured liveness or safety requirements.
BMC basically works like a breadth-first exploration of the state space, where
the (symbolic) transition relation is unwound up-to a predetermined bound un-
der the rationale that bugs appear even in the partially unfolded parts of the
state space. Rather than building a concrete representation of the state space,
a propositional formula is constructed representing the unfolded transition sys-
tem. A temporal logic formula is encoded on top of the propositional formula,
and the entire formula is subsequently handed over to a SAT solver. Much of
the research in BMC is therefore dedicated to finding more efficient and effective
propositional encodings for various classes of logics, e.g., for ACTL [20, 22] and
[]Lμ , the universal fragment of the μ-calculus [19].
The breadth-first exploration underlying BMC is also a weakness. The ef-
fectiveness of BMC is sensitive to the branching degree of the specification and
depends on the depth at which the property that is being checked occurs. High
branching degrees more quickly lead to a state explosion at shallower depths,
meaning that finding errors for deep and long-running properties is harder. This
is testified in e.g. [19].
In this paper, we take an alternative approach to bug-hunting, which we dub
Breadth-Bounded Model Checking (BBMC). Rather than restricting the num-
ber of unfoldings of the transition relation, BBMC restricts the breadth of the
exploration. In essence, we construct a homogeneous “slice” of the state space,
that we subsequently subject to verification using standard tooling. The slice
is constructed using algorithms that are based on a Highway simulation [10],
which is modified for the purpose of subsequent verification. We show that our
algorithms construct state spaces that are simulated by the full state space of
the symbolic input specification. The results by Loiseaux et al [17], regarding
the reflection of <>Lμ , the existential fragment of the μ-calculus (or, dually, the
preservation of []Lμ ), subsequently guarantees that any witness to an <>Lμ for-
mula, found in our state space is also in the original specification. This can be
used to find counterexamples for typical safety and liveness properties expressed
in []Lμ .
In order to obtain a good coverage of the inspected state space, BBMC
employs a uniform randomisation to construct a state space. A positive effect
of the randomisation is that successive runs increase the level of confidence in
the correctness of the input specification. We test the practical effectiveness
of BBMC, by subjecting the technique to several case studies. These vary in
size and complexity. The effectiveness is measured by offsetting the number of
states BBMC produces to the number of states BMC requires. The picture that
emerges from these experiments confirms our basic intuition: BMC generally
performs well on shallow properties, whereas BBMC performs better for prop-
erties at a deeper level and properties that require lengthier counterexamples.
This essentially means that BBMC and BMC are complementary.
- Login to post comments
