Development and Evaluation of a Framework for Parallelization of ProB

Author

Matthias Radig

Abstract

The ProB Animator and Model Checker enriches the formal development process with automatic and non-automatic exploration of a model’s states. Among its features are model and deadlock checking, model finding, and test-case generation. Because the number of different states a model can reach typically grows fast as the model is extended, the automatic exploration of the state space is often an expensive operation, which makes it worthwhile to search for ways of parallelizing these types of algorithms, so the work can be distributed among multiple computers. In this work we focus on the model checking algorithm. We explore the possibilities of distributed model checking with ProB to examine general problems related to dis- tributing automatic state exploration as well as issues that are a direct result of the ProB implementation. We develop a framework that abstracts the network layer and provides tools to measure performance and examine properties of the algorithms implemented on top of it, while also providing a runtime environment suitable to use ProB via its Java libraries. The framework is then used to implement a prototype distributed model checking algo- rithm. We examine how well the algorithm performs in terms of workload distribution and total runtime compared to the ProB model checker. We find that our system distributes the workload uniformly and scales sufficiently but re- quires about eight times as much computing power as the single-threaded model checker. A following detailed analysis shows that there is significant overhead introduced when exchanging states between the Java and Prolog processes. We conclude our work by proposing a number of improvements that reduce the need for expensive serialization and deserialization of states and therefore improve the efficiency of the algorithm.

Advised By

Jens Bendisposto, Michael Leuschel

Download: PDF