Skip to main content
Erschienen in:
Buchtitelbild

1999 | OriginalPaper | Buchkapitel

The Engineering of a Model Checker: the Gnu i-Protocol Case Study Revisited.

verfasst von : Gerard J. Holzmann

Erschienen in: Theoretical and Practical Aspects of SPIN Model Checking

Verlag: Springer Berlin Heidelberg

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Metadaten
Titel
The Engineering of a Model Checker: the Gnu i-Protocol Case Study Revisited.
verfasst von
Gerard J. Holzmann
Copyright-Jahr
1999
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/3-540-48234-2_18

Premium Partner