Skip Navigation



Journal of Logic and Computation Advance Access published online on March 5, 2009
Journal of Logic and Computation, doi:10.1093/logcom/exp004
This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Blom, S.
Right arrow Articles by Weber, M.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author, 2009. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Original Papers

A Database Approach to Distributed State-Space Generation

Stefan Blom

Institute of Computer Science, University of Innsbruck, Austria; Faculty of Electrical Engineering, Mathematics and Computer Science, University of Twente, The Netherlands.
E-mail: sccblom{at}cs.utwente.nl

Bert Lisser

Department of Software Engineering, CWI, The Netherlands.
E-mail: bert.lisser{at}cwi.nl

Jaco Van De Pol and Michael Weber

Department of Software Engineering, CWI, The Netherlands; Faculty for Electrical Engineering, Mathematics and Computer Science, University of Twente, The Netherlands.
E-mail: vdpol{at}cs.utwente.nl; michaelw{at}cs.utwente.nl

Received 29 February 2008.

We study distributed state-space generation on a cluster of workstations. It is explained why state-space partitioning by a global hash function is problematic when states contain variables from unbounded domains, such as lists or other recursive data types. Our solution is to introduce a database which maintains a global numbering of state values. We also describe tree compression, a technique of recursive state folding, and show that it is superior to manipulating plain state vectors. This solution is implemented and linked to the µCRL toolset, where state values are implemented as maximally shared terms (ATerms). However, it is applicable to other models as well, e.g. PROMELA or LOTOS models. Our experiments show the trade-offs between keeping the database global, replicated or local, depending on the available network bandwidth and latency.

Keywords: State-space partitioning; state collapsing; tree compression; µCRL



References

  1. Badban B, Fokkink W, Groote JF, Pang J, van de Pol J. Verification of a sliding window protocol in µCRL and PVS. Formal Aspects of Computing (2005) 17:342–388.[CrossRef][Web of Science]
  2. Bell A, Haverkort BR. Sequential and distributed model checking of Petri net specifications. Electronic Notes in Theoretical Computer Science (2002) 68:539–558.[CrossRef]
  3. Blom S, Calamé JR, Lisser B, Orzan S, Pang J, Pol Jvd, Torabi Dashti M, Wijs AJ. Distributed analysis with µCRL: a compendium of case studies. In: Tools and Algorithms for the Construction and Analysis of Systems 2007—Grumberg O, Huth M, eds. (2007) 683–689. Vol. 4424 of Lecture Notes in Computer Science.
  4. Blom S, Lisser B, van de Pol J, Weber M. A database approach to distributed state space generation. Electronic Notes in Theoretical Computer Science (2007) 198:17–32.[CrossRef]
  5. Blom S, van Langevelde I, Lisser B. Compressed and distributed file formats for labeled transition systems. Electronic Notes in Theoretical Computer Science (2003) 89:68–83.[CrossRef]
  6. Blom SCC, Fokkink WJ, Groote JF, Langevelde IAv, Lisser B, Pol JCvd. µCRL: a toolset for analysing algebraic specifications. In: Computer Aided Verification (CAV 2001)—Berry G, Comon H, Finkel A, eds. (2001) Springer. 250–254. Vol. 2102 of Lecture Notes in Computer Science.
  7. Brand MGJvd, de Jong HA, Klint P, Olivier PA. Efficient annotated terms. Software – Practice & Experience (2000) 30:259–291.[CrossRef][Web of Science]
  8. Chung M-Y, Ciardo G. Saturation NOW. In: Quantitative Evaluation of Systems (2004) 272–281.
  9. Ciardo G. Distributed and structured analysis approaches to study large and complex systems. In: European Educational Forum: School on Formal Methods and Performance Analysis—Brinksma E, Hermanns H, Katoen J-P, eds. (2000) Springer. 344–374. Vol. 2090 of Lecture Notes in Computer Science.
  10. Ciardo G, Gluckman J, Nicol D. Distributed state-space generation of discrete-state stochastic models. INFORMS Journal on Computing (1998) 10:82–93.[Abstract/Free Full Text]
  11. Ciardo G, Marmorstein RM, Siminiceanu R. Saturation unbound. In: Tools and Algorithms for the Construction and Analysis of Systems—Garavel H, Hatcliff J, eds. (2003) 379–393. Vol. 2619 of Lecture Notes in Computer Science.
  12. Fernandez J-C, Garavel H, Kerbrat A, Mateescu R, Mounier L, Sighireanu M. Cadp (Cæsar/Aldébaran development package): A protocol validation and verification toolbox. In: Proceedings of 8th Computer Aided Verification (CAV)—Alur R, Henzinger TA, eds. (1996) 437–440. Vol. 1102 of Lecture Notes in Computer Science.
  13. Franklin WR. On an improved algorithm for decentralized extrema finding in circular configurations of processors. Communications of the ACM (1982) 25:336–337.[CrossRef][Web of Science]
  14. Garavel H, Mateescu R, Bergamini D, Curic A, Descoubes N, Joubert C, Smarandache-Sturm I, Stragier G. DISTRIBUTOR and BCG_MERGE: Tools for distributed explicit state space generation. In: Tools and Algorithms for the Construction and Analysis of Systems—Hermanns H, Palsberg J, eds. (2006) 445–449. Vol. 3920 of Lecture Notes in Computer Science.
  15. Graf S, Richier J-L, Rodriguez C, Voiron J. What are the limits of model checking methods for the verification of real life protocols? In: Automatic Verification Methods for Finite State Systems—Sifakis J, ed. (1989) Springer. 275–285. Vol. 407 of Lecture Notes in Computer Science.
  16. Groote JF, Pang J, Wouters AG. A balancing act: analyzing a distributed lift system. In: Proceedings of the 6th Workshop on Formal Methods for Industrial Critical Systems—Gnesi S, Ultes-Nitsche U, eds. (2001) INRIA Press. 1–12.
  17. Holzmann GJ. State compression in SPIN: Recursive indexing and compression training runs. In. Proceedings of 3rd International SPIN Workshop (1997).
  18. Luttik S. Description and formal specification of the link layer of P1394. In: Technical Report SEN-R9706 (1997) CWI.
  19. Pang J, Fokkink WJ, Hofman RF, Veldema R. Model checking a cache coherence protocol of a Java DSM implementation. JLAP (2007) 71:1–43.
  20. Sighireanu M, Mateescu R. Verification of the link layer protocol of the IEEE-1394 serial bus (FireWire): an experiment with E-LOTOS. STTT (1998) 2:68–88.
  21. Stern U, Dill DL. Parallelizing the Mur{phi} verifier. Grumberg O, ed. (1997) Springer. 256–267. In Computer-Aided Verification, 9th International Conference, Vol. 1254 of Lecture Notes in Computer Science.
  22. Visser W, Barringer H. Memory efficient state storage in SPIN. In: The Spin Verification System, DIMACS Series in Discrete Mathematics and Theoretical Computer Science—Grégoire J-C, Holzmann GJ, Peled D, eds. (1997) 32. American Mathematical Society.
  23. Weber M. An embeddable virtual machine for state space generation. In: Proceedings of 14th SPIN Workshop—Bosnacki D, Edelkamp S, eds. (2007) Springer. 168–185. Vol. 4595 of Lecture Notes in Computer Science.

Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?



This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Blom, S.
Right arrow Articles by Weber, M.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?