From Abstract Distributed Model Checking to Concrete Implementation

Christophe Joubert


Distributed Model-Checking (DMC) has become a very valuable technique for computer system verification. However, due to its inherent complexity, it is not very accessible for non-experts in verification methods and distributed programming. DMC requires a number of interleaved distributed algorithms, which make it complex and cumbersome. In this paper, we consider one fundamental aspect of DMC design. Message passing mechanisms that can lead distributed systems to deadlock or high overhead, present hidden tradeoffs often dismissed in the literature. We illustrate our discussion using a generic distributed state space generation algorithm. Key words: distributed and parallel computing, message passing, state space generation, model checking