Methods to Model-Check Parallel Systems Software

TL;DR

This paper explores formal verification methods for MPD, a distributed system, comparing model checking with SPIN and theorem proving with OTTER to evaluate their effectiveness and scalability.

Contribution

It introduces two verification approaches for MPD and analyzes their modeling methodology, performance, and scalability.

Findings

SPIN effectively verifies MPD components using model checking.

OTTER provides an alternative theorem-proving approach for system verification.

Performance varies significantly between the two methods depending on system complexity.

Abstract

We report on an effort to develop methodologies for formal verification of parts of the Multi-Purpose Daemon (MPD) parallel process management system. MPD is a distributed collection of communicating processes. While the individual components of the collection execute simple algorithms, their interaction leads to unexpected errors that are difficult to uncover by conventional means. Two verification approaches are discussed here: the standard model checking approach using the software model checker SPIN and the nonstandard use of a general-purpose first-order resolution-style theorem prover OTTER to conduct the traditional state space exploration. We compare modeling methodology and analyze performance and scalability of the two methods with respect to verification of MPD.