Rebeca Breadth First Search (BFS) Model Checker:
We developed Rebeca BFS model checker with the goal of developing a distributed model checker for Rebeca (2009-2010).
Rebeca BFS model checker creates and explores system state space level by level and examines back edges of
the state space graph for cycle detection. In the first step of BFS model checking, the initial state of
the model is created, marked as visited and its level is set to zero. The synchronous product of this
state and the initial state of the property is stored as the system initial state. Then the direct successors
of the initial states of the model and the property are generated by applying successor function.
Synchronous products of these newly generated states (of model and property) are stored as system level one
states. Generating the states of the next levels and on-the-fly synchronous product creates the whole
state space of the system.
* The first direct model checking tool for Rebeca is Modere model checker and is developed in 2005.
Modere is implemented based on nested-DFS algorithm (More about Modere in
ICDCIT'05,
SAC'06 and
Acta Informatica).
Rebeca Distributed BFS Model Checker:
Model checking, as a widely used technique for automatic verification, faces
the state space explosion phenomena. Execution of medium and large systems
produce high number of states and because of the memory limits state space
explosion occurs. One of the approaches for overcoming the state space explosion
is distributing state space among some nodes. Applying this technique on model
checking, results in development of parallel and distributed model checkers.
According to the above reasons we have developed distributed BFS model checker
of Rebeca. The major difference between centralized and distributed Rebeca BFS
model checking (BFS-MC) algorithms is in storing next level states. In the
centralized BFS-MC, all the newly generated system states are stored in the
next level states queue but in the distributed BFS-MC, some of them are sent
to the other nodes of the cluster. In the other words, each state has a host
node. Host of a state is the node which is responsible for storing the state
and generating its successors.
The other difference between centralized and distributed BFS-MC is cluster
nodes synchronization at the end of each iteration. In the synchronization,
nodes that finish processing of their current level states earlier than
others shall wait for other nodes to finish their work. So after synchronization,
all nodes have processed their current level states and all of them are ready
to continue the search for the next level.
Call Dependency Graph for Rebeca Distributed BFS Model Checker:
In the distributed model checking state distribution policy has an important
role in the algorithm performance. The general and widely used approach is
computing hash value for the state and assigning the state to the host
according to a uniform distribution based on the hash value. The random
distribution saves the nodes load balancing but increases the split
cycles of state space graph.
To reduce split edges, we have developed a technique to manage state
distribution based on static analysis of model. Our algorithm finds the
call dependency graph (CDG) of model actors and sends the state based on
the cycles of CDG.
The current release version of the tool and a couple of examples are available
here.
To process the examples provided please read the
instructions first.