Stephen F. Siegel, Samuel E. Moelius III, and Louis F. Rossi, A
Case Study in the Use of Model Checking to Verify Parallel
Scientific Software,
Technical Report UDEL-CIS 2007/343, Department of
Computer and Information Sciences, University of Delaware,
November 12, 2007.
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.
@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"
}
