Skip to main content
SpringerLink
Log in

Characterising Testing Preorders for Broadcasting Distributed Systems

  • Conference paper
  • First Online:
Trustworthy Global Computing (TGC 2014)

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

Included in the following conference series:

Abstract

We present a process calculus for both specifying the desired behaviour of distributed systems and for describing their actual implementation; the calculus is aimed at the internet layer of the TCP/IP reference model. This allows us to define behavioural preorders in the style of DeNicola and Hennessy, relating specifications and implementations for distributed systems at this level of abstraction. The main result of the paper is a complete characterisation of these preorders, for a large class of systems, in terms of traces of extensional actions. This result underpins a sound and complete proof methodology which is demonstrated by the verification of the correct behaviour of a virtual shared memory protocol.

Supported by SFI project SFI 06 IN.1 1898.

Andrea Cerone: Supported by SFI project SFI 06 IN.1 1898.

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 34.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 44.99
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. Bugliesi, M., Gallina, L., Marin, A., Rossi, S., Hamadou, S.: Interference-sensitive preorders for manets. In: QEST, pp. 189–198 (2012)

    Google Scholar 

  2. Cerone, A.: Foundations of Ad Hoc Wireless Networks. PhD thesis, Trinity College Dublin (2012). http://software.imdea.org/~andrea.cerone/works/thesis.pdf

  3. Cerone, A., Hennessy, M.: Modelling probabilistic wireless networks. LMCS 9(3) (2013)

    Google Scholar 

  4. Cerone, A., Hennessy, M.: Characterising testing preorders for broadcasting distributed systems (extended version) (2014). http://software.imdea.org/~andrea.cerone/works/TGC14extended.pdf

  5. Cerone, A., Hennessy, M., Merro, M.: Modelling MAC-Layer Communications in Wireless Systems. In: De Nicola, R., Julien, C. (eds.) COORDINATION 2013. LNCS, vol. 7890, pp. 16–30. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  6. Daws, C., Kwiatkowska, M.Z., Norman, G.: Automatic verification of the ieee-1394 root contention protocol with kronos and prism. Electr. Notes Theor. Comput. Sci. 66(2), 104–119 (2002)

    Article  Google Scholar 

  7. De Nicola, R., Hennessy, M.: Testing equivalences for processes. TCS 34, 83–133 (1984)

    Article  MATH  Google Scholar 

  8. Ene, C.F., Muntean, T.: Testing theories for broadcasting processes. Sci. Ann. Cuza Univ. 11, 214–230 (2002)

    MATH  MathSciNet  Google Scholar 

  9. Ghassemi, F., Fokkink, W., Movaghar, A.: Equational reasoning on mobile ad hoc networks. Fund. Inf. 105(4), 375–415 (2010)

    MATH  MathSciNet  Google Scholar 

  10. Hennessy, M., Rathke, J.: Bisimulations for a calculus of broadcasting systems. TCS, 200 (1998)

    Google Scholar 

  11. Lanese, I., Sangiorgi, D.: An operational semantics for a calculus for wireless systems. TCS 411(19), 1928–1948 (2010)

    Article  MATH  MathSciNet  Google Scholar 

  12. Lerda, F., Sisto, R.: Distributed-Memory Model Checking with SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 22–39. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  13. Merro, M., Ballardin, F., Sibilio, E.: A timed calculus for wireless systems. TCS 412(47), 6585–6611 (2011)

    Article  MATH  MathSciNet  Google Scholar 

  14. Milner, R.: A calculus of communicating systems. LNCS, 92 (1980)

    Google Scholar 

  15. Musuvathi, M., Engler, D.R.: Model checking large network protocol implementations. In: NSDI, pp. 155–168 (2004)

    Google Scholar 

  16. Nanz, S., Hankin, C.: A framework for security analysis of mobile wireless networks. TCS, 367 (2006)

    Google Scholar 

  17. Nanz, S., Hankin, C.: Static analysis of routing protocols for ad-hoc networks (March 25, 2004)

    Google Scholar 

  18. Prasad, K.: A calculus of broadcasting systems. SCP, 25 (1995)

    Google Scholar 

  19. Singh, A., Ramakrishnan, C.R., Smolka, S.A.: A process calculus for mobile ad hoc networks. SCP 75(6), 440–469 (2010)

    MATH  MathSciNet  Google Scholar 

  20. Tanenbaum, A.S.: Computer Networks. 4th ed. Prentice Hall PTR (2002)

    Google Scholar 

  21. Wang, M., Lu, Y.: A timed calculus for mobile ad hoc networks. arXiv preprint arXiv:1301.0045 (2013)

Download references

Author information

Authors and Affiliations

  1. IMDEA Software Institute, Madrid, Spain

    Andrea Cerone

  2. Trinity College Dublin, Dublin, Ireland

    Matthew Hennessy

Authors
  1. Andrea Cerone
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Matthew Hennessy
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Andrea Cerone .

Editor information

Editors and Affiliations

  1. Department of Computer Science, Saarland University, Saarbrücken, Germany

    Matteo Maffei

  2. Computer Science, University of Leicester, Leicester, United Kingdom

    Emilio Tuosto

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cerone, A., Hennessy, M. (2014). Characterising Testing Preorders for Broadcasting Distributed Systems. In: Maffei, M., Tuosto, E. (eds) Trustworthy Global Computing. TGC 2014. Lecture Notes in Computer Science(), vol 8902. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-45917-1_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-45917-1_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-45916-4

  • Online ISBN: 978-3-662-45917-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation