Methods to Model-Check Parallel Systems Software

Title: Methods to Model-Check Parallel Systems Software

Research Question: How can we effectively verify the correctness of parallel systems software like the Multi-Purpose Daemon (MPD)?

Methodology: The researchers used two verification approaches: 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. They compared modeling methodology and analyzed performance and scalability of the two methods with respect to verifying MPD.

Results: The study found that both methods were effective in verifying the MPD system. The Spin-based approach was more straightforward, while the Otter-based approach was more flexible and scalable. The researchers also compared the modeling methodologies and found that the Otter approach was more expressive and allowed for better abstraction.

Implications: The research highlights the potential of formal verification techniques in ensuring the correctness of parallel systems software. It also provides insights into the choice of verification methodology based on the specific requirements and constraints of the software under consideration. The study suggests that a combination of both approaches could be beneficial for large-scale systems.

Link to Article: https://arxiv.org/abs/0312012v1 Authors: arXiv ID: 0312012v1