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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Y. Dong, X. Du, et al., Fighting livelock in the i-protocol: a comparative study of verification tools. Proc. TACAS99, Amsterdam, The Netherlands, March 1999.
Y. Dong and C.R. Ramakrishnan. An optimizing compiler for efficient model checking. Unpublished manuscript, available from: http://www.cs.sunysb.edu/~lmc/papers/compiler/.
G.J. Holzmann, D. Peled, An improvement in formal verification, Proc. Conf. on Formal Description Techniques, Proc. FORTE94, Berne, Switzerland, 1994.
G.J. Holzmann, State Compression in Spin, Proc. Third Spin Workshop, April 1997, Twente University, The Netherlands.
—, The model checker Spin, IEEE Trans. on Software Engineering, Vol.23, No. 5, May 1997, pp. 279–295.
— and A. Puri, A Minimized Automaton Representation of Reachable States, Software Tools for Technology Transfer, Springer Verlag, Vol. 3, No. 1, 1999.
—, Designing executable abstractions, Proc. Workshop on Formal Methods in Software Practice, Clearwater Beach, Fl., March 1998, ACM Press.
— and M.H. Smith, A practical method for the verification of event driven software. Proc. ICSE99, Int. Conf. on Software Engineering, Los Angeles, CA, May 1999, pp. 597–607.
K. McMillan, Symbolic model checking. Kluwer Academic, 1993.
Y.S. Ramakrishna, C.R. Ramakrishnan, et al., Efficient model checking using tabled resolution. Proc. CAV97, LNCS 1254, pp. 143–154, Springer Verlag.
HY. van der Schoot and H. Ural, An improvement on partial order model checking with ample sets. Computer Science Technical Report, TR-96-11, Univ. of Ottawa, Canada, Sept. 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Holzmann, G.J. (1999). The Engineering of a Model Checker: the Gnu i-Protocol Case Study Revisited.. In: Dams, D., Gerth, R., Leue, S., Massink, M. (eds) Theoretical and Practical Aspects of SPIN Model Checking. SPIN 1999. Lecture Notes in Computer Science, vol 1680. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48234-2_18
Download citation
DOI: https://doi.org/10.1007/3-540-48234-2_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66499-4
Online ISBN: 978-3-540-48234-5
eBook Packages: Springer Book Archive