Abstract
In this paper we propose a distributed algorithm for model- checking LTL. In particular, we explore the possibility of performing nested depth-first search algorithm in distributed SPIN. A distributed version of the algorithm is presented, and its complexity is discussed.
This work has been supported in part by the Grant Agency of Czech Republic grants
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
S. Aggarwal, R. Alonso, and C. Courcoubetis. Distributed reachability analysis for protocol verification environments. In P. Varaiya and H. Kurzhanski, editors, Discrete Event Systems: Models and Application, volume 103 of LNCIS, pages 40–56, Berlin, Germany, August 1987. Springer-Verlag.
J. Barnat, L. Brim, and J. Stříbrná. Distributed LTL Model-Checking in SPIN. Technical Report FI-MU-10/00, Masaryk Univeristy Brno, 2000.
S. Ben-David, T. Heyman, O. Grumberg, and A. Schuster. Scalable distributed on-the-fly symbolic model checking. In third International Conference on Formal methods in Computer-Aided Design (FMCAD’00), Austin, Texas, November 2000.
David L. Dill. The murϕ verification system. In Conference on Computer-Aided Verification (CAV’ 96), Lecture Notes in Computer Science, pages 390–393. Springer-Verlag, July 1996.
Tamir Heyman, Danny Geist, Orna Grumberg, and Assaf Schuster. Achieving scalability in parallel reachability analysis of very large circuits. In Orna Grumberg, editor, Computer Aided Verification, 12th International Conference, volume 1855 of Lecture Notes in Computer Science, pages 20–35. Springer-Verlag, June 2000.
G.J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs, New Jersey, 1991.
Gerard J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279–295, May 1997. Special Issue: Formal Methods in Software Practice.
F. Lerda and R. Sisto. Distributed-memory model checking with SPIN. In SPIN workshop, number 1680 in LNCS, Berlin, 1999. Springer.
Robert Tarjan. Depth first search and linear graph algorithms. SIAM journal on computing, pages 146–160, January 1972.
U. Stern and D. L. Dill. Parallelizing the murϕ verifier. In O. Grumberg, editor, Proceedings of Computer Aided Verification (CAV’ 97), volume 1254 of LNCS, pages 256–267, Berlin, Germany, 1997. Springer.
P. Wopler and D. Leroy. Reliable hashing without collision detection. In Conference on Computer-Aided Verification (CAV’ 93), Lecture Notes in Computer Science, pages 59–70. Springer-Verlag, 1993.
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
Barnat, J., Brim, L., Stříbrná, J. (2001). Distributed LTL model-checking in SPIN. In: Dwyer, M. (eds) Model Checking Software. SPIN 2001. Lecture Notes in Computer Science, vol 2057. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45139-0_13
Download citation
DOI: https://doi.org/10.1007/3-540-45139-0_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42124-5
Online ISBN: 978-3-540-45139-6
eBook Packages: Springer Book Archive