Computer Science – Logic in Computer Science
Scientific paper
2003-12-05
Computer Science
Logic in Computer Science
12 pages, 3 figures, 1 table
Scientific paper
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.
Lusk Ewing
Matlin Olga Shumsky
McCune William
No associations
LandOfFree
Methods to Model-Check Parallel Systems Software does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Methods to Model-Check Parallel Systems Software, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Methods to Model-Check Parallel Systems Software will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-474660