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.
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.
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.
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.