Title: A Case Study in the Use of Model Checking to Verify Parallel Scientific Software
Authors: Stephen F. Siegel, Samuel E. Moelius III, and Louis F. Rossi
Abstract:
We report on a case study using the model checking tool MPI-Spin to verify a nontrivial, deployed, MPI-based scientific program. The program, BlobFlow/ECCSVM, is an open source code implementing a high order vortex method for solving the Navier-Stokes equations in two dimensions. Over the past several years, it has been used for a variety of applications, including jets, coherent vortex structures, and fluid-structure interactions. Despite the size and complexity of the code, we are able to verify not only data-independent properties such as freedom from deadlock, but also the functional equivalence of the sequential and parallel versions of the program, under certain restrictions. Our ``lessons learned'' include new insights into the technology that will be required to automate the modeling and verification process for complex scientific software.
Appeared in:
Technical Report UDEL-CIS 2007/343, Department of Computer and Information Sciences, University of Delaware, November 12, 2007.
BibTeX:
@TechReport{siegel-rossi:2007:eccsvm_tr,
author = "Stephen F. Siegel and Sameuel E. Moelius III and Louis F. Rossi",
title = "A Case Study in the Use of Model Checking to Verify Parallel Scientific Software",
institution = "Department of Computer and Information Sciences, University of Delaware",
year = 2007,
month = nov,
number = "UDEL-CIS 2007/343"
}
Download:
Related Links: