Skip to main content
SpringerLink
Log in

Gossiping Girls Are All Alike

  • Conference paper
Model Checking Software (SPIN 2012)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7385))

Included in the following conference series:

Abstract

This paper discusses several different ways to model the well-known gossiping girls problem in promela. The highly symmetric nature of the problem is exploited using plain promela, topspin (an extension to Spin for symmetry reduction), and by connecting Spin to bliss (a tool to compute canonical representations of graphs). The model checker Spin is used to compare the consequences of the various modelling choices.

This – tutorial style – paper is meant as a road map of the various ways of modelling symmetric systems that can be explored.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 72.00
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bosnacki, D., Dams, D., Holenderski, L.: Symmetric Spin. STTT 4(1), 92–106 (2002)

    Article  Google Scholar 

  2. Donaldson, A.F., Miller, A.: A Computational Group Theoretic Symmetry Reduction Package for the Spin Model Checker. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol. 4019, pp. 374–380. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  3. Edelkamp, S., Lluch Lafuente, A., Leue, S.: Directed Explicit Model Checking with HSF-SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 57–79. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  4. Emerson, E.A., Trefler, R.J.: From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 142–157. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  5. Emerson, E.A., Wahl, T.: On Combining Symmetry Reduction and Symbolic Representation for Efficient Model Checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 216–230. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  6. Holzman, G.J.: The Spin Model Checker – Primer and Reference Manual. Addison-Wesley, Boston (2003)

    Google Scholar 

  7. Holzmann, G.J., Joshi, R.: Model-Driven Software Verification. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 76–91. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  8. Holzmann, G.J., Joshi, R., Groce, A.: Tackling Large Verification Problems with the Swarm Tool. In: Havelund, K., Majumdar, R. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 134–143. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  9. Hurkens, C.: Spreading gossip efficiently. Nieuw Archief Voor Wiskunde 5/1(2), 208–210 (2000)

    MathSciNet  Google Scholar 

  10. Junttila, T., Kaski, P.: Engineering an Efficient Canonical Labeling Tool for Large and Sparse Graphs. In: Applegate, D., Brodal, G.S., Panario, D., Sedgewick, R. (eds.) Proc. of ALENEX 2007, pp. 135–149. SIAM (2007)

    Google Scholar 

  11. Katoen, J.-P.: How to Model and Analyze Gossiping Protocols? acm sigmetrics’ Performance Evaluation Review 36(3), 3–6 (2008)

    Article  Google Scholar 

  12. Liben-Nowell, D.: Gossip is Synteny: Incomplete Gossip and the Syntenic Distance between Genomes. Journal of Algorithms 43(2), 264–283 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  13. Pnueli, A., Xu, J., Zuck, L.D.: Liveness with (0,1, ∞ )-Counter Abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 107–122. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  14. Pong, F., Dubois, M.: A New Approach for the Verification of Cache Coherence Protocols. IEEE Transactions on Parallel and Distributed Systems 6(8), 773–787 (1995)

    Article  Google Scholar 

  15. Rensink, A.: The GROOVE Simulator: A Tool for State Space Generation. In: Pfaltz, J.L., Nagl, M., Böhlen, B. (eds.) AGTIVE 2003. LNCS, vol. 3062, pp. 479–485. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  16. Rensink, A.: Isomorphism Checking in groove. In: Zündorf, A., Varró, D. (eds.) Proc. of Graph-Based Tools, GraBaTs 2006, Natal, Brazil. Electronic Communications of the EASST, vol. 1 (2006)

    Google Scholar 

  17. Rensink, A., Kuperus, J.-H.: Repotting the Geraniums: On Nested Graph Transformation Rules. In: Boronat, A., Heckel, R. (eds.) Proc. of Graph Transformation and Visual Modeling Techniques, York, UK. Electronic Communications of the EASST, vol. 18 (March 2009)

    Google Scholar 

  18. Ruys, T.C.: Low-Fat Recipes for Spin. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 287–321. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  19. Ruys, T.C.: Towards Effective Model Checking. PhD thesis, University of Twente, Enschede, The Netherlands (March 2001)

    Google Scholar 

  20. Ruys, T.C.: Optimal Scheduling Using Branch and Bound with SPIN 4.0. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 1–17. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  21. Seindal, R.: GNU m4, version 1.4.16. Free Software Foundation, Inc., 1.4.16 edition (2011), http://www.gnu.org

  22. Vaandrager, F.W.: A First Introduction to uppaal. In: Tretmans, G.J. (ed.) Quasimodo Handbook. Springer (to appear, 2012)

    Google Scholar 

  23. bliss – A Tool for Computing Automorphism Groups and Canonical Labelings of Graphs, http://www.tcs.hut.fi/Software/bliss/

  24. gap – system for computational discrete algebra, http://www.gap-system.org/

  25. groove – graphs for object-oriented verification, http://groove.cs.utwente.nl/

  26. Saucy2 – Fast Symmetry Discovery, http://vlsicad.eecs.umich.edu/BK/SAUCY/

  27. swarm - verification script generator for Spin, http://www.spinroot.com/swarm/

  28. topspin, http://www.doc.ic.ac.uk/~afd/topspin/

Download references

Author information

Authors and Affiliations

  1. RUwise, The Netherlands

    Theo C. Ruys

  2. Ordina, The Netherlands

    Pim Kars

Authors
  1. Theo C. Ruys
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pim Kars
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing, Imperial College London, 180 Queen’s Gate, SW7 2BZ, London, UK

    Alastair Donaldson

  2. School of Computer Science, University of Birmingham, B15 2TT, Edgbaston, Birmingham, UK

    David Parker

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ruys, T.C., Kars, P. (2012). Gossiping Girls Are All Alike. In: Donaldson, A., Parker, D. (eds) Model Checking Software. SPIN 2012. Lecture Notes in Computer Science, vol 7385. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31759-0_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-31759-0_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-31758-3

  • Online ISBN: 978-3-642-31759-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation