Abstract
This paper describes a reduction technique which is very useful against the state explosion problem which occurs when model checking many distributed systems. Timestamps are often used to keep track of the relative order of events. They are usually implemented with very large counters and therefore they generate state explosion. The aim of this paper is to present a very efficient reduction of the state space generated by a model checker when using timestamps. The basic idea is to map the timestamps values to the smallest possible range. This is done dynamically and on-the-fly by adding to the model checker a call to a reduction function after each newly generated state. Our reduction works for model checkers using explicit state enumeration and does not require any change in the model. Our method has been applied to an industrial example and the reduction obtained was spectacular.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
G. J. Holzmann. The Spin Model Checker. IEEE Trans. on Software Engineering, 23(5):279–295, May 1997.
T. Bolognesi and E. Brinksma. Introduction to the ISO Speci_cation Language lotos. Computer Networks and ISDN Systems, pages 25–59, 1987.
M. Plath and M. Ryan. Plug and Play Features. Fifth International Workshop on Feature Interactions in Telecommunications and Software Systems, 1998. IOS Press.
C. Pecheur. Advanced Modeling and Verification Techniques Applied to a Cluster File System. Proc. of the 14th IEEE International Conference on Automated Software Engineering ASE-99, October 1999.
H. Garavel and L. Mounier. Specification and Verification of Various Distributed Leader Election Algorithms for Unidirectional Ring Networks. Science of Computer Programming, 29(1-2):171–197, 1997.
M. Calder and A. Miller. Analyzing a Basic Call Protocol Using Promela/Xspin. Fourth International Spin Workshop, Nov. 1998.
P. Godefroid. ”Partial-Order Methods for the Verification of Concurrent Systems-An Approach to the State-Explosion Problem, volume 1032 of Lecture Notes in Computer Science. Springer-Verlag, January 1996. ISBN 3-540-60761-7.
D. Peled. Partial-Order Reductions: Model Checking Using Representatives. In Proc. of MFCS’96, number 1113 in Lecture Notes in Computer Science, pages 93–112. Springer-Verlag, 1996.
C. Norris Ip and D. L. Dill. Better Verification Through Symmetry. Formal Methods in System Design, 9(1/2):41–75, August 1996.
T. P. Petrov, A. Pogosyants, S. J. Garland, V. Luchangco, and N. A. Lynch. Computer-Assisted Verification of an Algorithm for Concurrent Timestamps. In Reinhard Gotzhein and Jan Bredereke, editors, Formal Description Techniques IX: Theory, Applications, and Tools, pages 29–44. Chapman & Hall, 1996.
R. Khazan, A. Fekete, and N. A. Lynch. Multicast Group Communication as a Base for a Load-Balancing Replicated Data Service. DISC’ 98(formerly WDAG) 12th International Symposium on DIStributed Computing, 1998.
N. A. Lynch and M. R. Tuttle. An Introduction to Input/Output Automata. CWI-Quaterly, 2(3):219–246, September 1989.
S. Garland and J. Guttag. A Guide to lp, the Larch Prover. Technical Report 82, DEC Systems Research Center, 1991.
R. Guerraoui and A. Schiper. Fault-Tolerance by Replication in Distributed Systems. Reliable Software Technologies-Ada Europe’ 96. Lecture Notes in Computer Science, 1088, 1996.
D. R. Cheriton and D. Skeen. Understanding the Limitations of Causally and Totally Ordered Communication. Proc. of the 14th Symposium on Operating Systems Principles, December 1993.
M. Raynal, A. Schiper, and S. Toueg. The Causal Ordering Abstraction and a Simple Way to Implement It. IPL, 39(6):343–350, 1991.
K. Birman, A. Schiper, and P. Stephenson. Lightweight Causal and Atomic Group Multicast. ACM Trans. on Computer Systems, pages 272–314, August 1991.
A. Israåli and M. Li. Bounded Time-Stamps. Proc 28th IEE Symposium on Foundations of Computer Science, pages 371–382, 1987.
D. Dolev and N. Shavit. Bounded Concurrent Time-Stamping. SIAM Journal on Computing, 26(2):418–455, April 1997.
R. Cori and E. Sopena. Some Combinatorial Aspects of Time-Stamp Systems. European Journal of Combinatorics, pages 95–102, 1993.
A. Pnueli. The Temporal Logic of Programs. Proc 18th IEEE Symp. Foundations of Computer Science, pages 46–57, 1977.
E.A. Emerson. Temporal and Modal Logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 16, pages 995–1072. Elsevier Publ. Co., Amsterdam, 1990.
C. J. Fidge. Timestamps in Message-Passing Systems that Preserve the Partial Ordering. Australian Computer Science Communications, 10(1):56–66, February 1988.
F. Mattern. Virtual Time and Global States of Distributed Systems. In M. Cosnard et al., editor, Parallel and Distributed Algorithms, pages 215–226. North-Holland, 1989.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Derepas, F., Gastin, P., Plainfossé, D. (2001). Avoiding State Explosion for Distributed Systems with Timestamps. In: Oliveira, J.N., Zave, P. (eds) FME 2001: Formal Methods for Increasing Software Productivity. FME 2001. Lecture Notes in Computer Science, vol 2021. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45251-6_7
Download citation
DOI: https://doi.org/10.1007/3-540-45251-6_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41791-0
Online ISBN: 978-3-540-45251-5
eBook Packages: Springer Book Archive