The Engineering of a Model Checker: the Gnu i-Protocol Case Study Revisited.
- 27 August 1999
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
- p. 232-244
- https://doi.org/10.1007/3-540-48234-2_18
Abstract
In a recent study a series of model checkers, among which Spin [5], SMV [9], and a newer system called XMC [10], were compared on performance. The measurements used for this comparison focused on a model of the i-protocol from GNU uucp version 1.04. Eight versions of this iprotocol model were obtained by varying window size, assumptions about the transmission channel, and the presence or absence of a patch for a known livelock error. The results as published in [1] show the XMC system to outperform the other model checking systems on most of the tests. It also contains a challenge to the builders of the other model checkers to match the results. This paper answers that challenge for the Spin model checker. We show that with either default Spin verification runs, or a reasonable choice of parameter settings, the version of Spin that was used for the tests in [1] (Spin 2.9.7) can outperform the results obtained with XMC in six out of eight tests. Inspired by the comparisons, and the description in of the optimizations used in XMC, we also extended Spin with some of the same optimizations, leading to a new Spin version 3.3.0. We show that with these changes Spin can outperform XMC on all eight tests.Keywords
This publication has 4 references indexed in Scilit:
- Fighting Livelock in the i-Protocol: A Comparative Study of Verification ToolsLecture Notes in Computer Science, 1999
- The model checker SPINIEEE Transactions on Software Engineering, 1997
- Efficient model checking using tabled resolutionLecture Notes in Computer Science, 1997
- Symbolic Model CheckingPublished by Springer Science and Business Media LLC ,1993