Franck van Breugel is a professor at the Department of Computer
Science and Engineering of York University, which is located in
Toronto, Canada. He founded and leads the DisCoVeri group whose
members carry out research in the areas of distributed computing,
Verification of the source code of a probabilistic system by means of
an explicit-state model-checker is challenging. In most cases, the
probabilistic model-checker will run out of memory due to the infamous
state space explosion problem. In this talk, we introduce the notion
of a progress measure for such a model-checker. The progress measure
returns a number in the interval [0, 1]. This number provides us a
quantitative measure of the amount of progress the model-checker has
made with verifying a particular linear-time property. The larger the
number, the more progress the model-checker has made. In particular,
the progress measure provides a lower-bound of the measure of the set
of execution paths that satisfy the property.
Java PathFinder (JPF) in an explicit-state model-checker for Java
bytecode. We have extended JPF to a probabilistic model-checker.
JPF can traverse the state space in different ways, including
depth-first and breadth-first. With the additional probabilistic
information available to JPF, new traversal strategies can be added
to JPF. We present a few simple traversal strategies that take the
probabilities into account.
We have extended JPF so that it keeps track of the amount of progress
it has made with checking invariants. We show the difference in
progress of the different traversal strategies for a few examples.
This is joint work with Elise Cormie-Bowins and Xin Zhang.