Distributed modular model checking

Abstract

Summary form only given. Model checking is a formal method that verifies whether a finite state model of a system satisfies a specification given as a temporal logic formula. The most severe problem model checking suffers from is the so called state explosion problem. Distribution is one of the techniques that combat the state explosion. The aim is to distribute the state space among a number of computers so as to be able to verify larger systems. Another approach that deals with the state explosion problem is modularity, i.e. exploiting the structure of the system. We propose to employ modular techniques to the distributed model checking problem. This can be useful especially for software, as the software model checking algorithms suffer from state explosion more severely than the hardware model checking techniques even when the system consists of one sequential finite-state component. Moreover, software programs have typically richer syntactic structure that can be exploited. Besides elaborating a theoretical background for distributed model checking based on the modular approach, we also intend to develop modular approaches to partitioning the state space, in particular to define partition functions that reduce the necessary communication in the distributed environment.