Skip to main content
SpringerLink
Log in

Channel Representations in Protocol Verification

Preliminary Version

  • Conference paper
  • First Online:
Book cover CONCUR 2001 — Concurrency Theory (CONCUR 2001)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2154))

Included in the following conference series:

Abstract

In automated verification of protocols, one source of complications is that channels may have unbounded capacity, in which case a naive model of the protocol is no longer finite state. Symbolic techniques have therefore been developed for representing the contents of unbounded channels. In this paper, we survey some of these techniques and apply them to a simple leader election protocol. We consider protocols with entities modeled as finite state machines which communicate by sending messages from a finite alphabet over unbounded channels; this is a framework for which many techniques have been developed. We also consider a more general model in which messages may belong to an unbounded domain of values which may be compared according to a total ordering relation: the motivation is to study protocols with timestamps or priorities. We show how techniques from the previous setting can be extended to this more general model, but also show that reachability quickly becomes undecidable if channels preserve the ordering between messages.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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. Parosh Aziz Abdulla, Aurore Annichini, and Ahmed Bouajjani. Algorithmic verification of lossy channel systems: An application to the bounded retransmission protocol. In Proc. TACAS’ 99, volume 1579 of LNCS, 1999.

    Google Scholar 

  2. Parosh Aziz Abdulla, Luc Boasson, and Ahmed Bouajjani. Effective lossy queue languages, 2001. To appear in Proc. ICALP’ 2001: 28th International Colloquium on Automata, Lnaguages, and Programming.

    Google Scholar 

  3. Parosh Aziz Abdulla, Ahmed Bouajjani, and Bengt Jonsson. On-the-fly analysis of systems with unbounded, lossy fifo channels. In Proc. 10th Int. Conf. on Computer Aided Verification, volume 1427 of LNCS, pages 305–318, 1998.

    Google Scholar 

  4. Parosh Aziz Abdulla, Karlis Cer↭s, Bengt Jonsson, and Tsay Yih-Kuen. General decidability theorems for infinite-state systems. In Proc. LICS’ 96 11 th IEEE Int. Symp. on Logic in Computer Science, pages 313–321, 1996.

    Google Scholar 

  5. Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. Information and Computation, 127(2):91–101, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  6. Parosh Aziz Abdulla and Bengt Jonsson. Verifying networks of timed processes. In Bernhard Steffen, editor, Proc. TACAS’ 98, volume 1384 of LNCS, pages 298–312, 1998.

    Google Scholar 

  7. Parosh Aziz Abdulla and Aletta Nyl’en. Timed Petri nets and BQOs, 2001. To appear in Proc. ICATPN’2001: 22nd Int. Conf. on application and theory of Petri nets.

    Google Scholar 

  8. T.P. Blumer and D.P. Sidhu. Mechanical verification of communication protocols. IEEE Trans. on Software Engineering, SE-12(8):827–843, Aug. 1986.

    Google Scholar 

  9. B. Boigelot and P. Godefroid. Symbolic verification of communication protocols with infinite state spaces using QDDs. In Alur and Henzinger, editors, Proc. 8 th Int. Conf. on Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 1–12. Springer Verlag, 1996.

    Google Scholar 

  10. B. Boigelot, P. Godefroid, B. Willems, and P. Wolper. The power of QDDs. In Proc. of the Fourth International Static Analysis Symposium, LNCS. Springer Verlag, 1997.

    Google Scholar 

  11. A. Bouajjani and P. Habermehl. Symbolic reachability analysis of fifo-channel systems with nonregular sets of configurations. In Proc. ICALP’ 97, volume 1256 of Lecture Notes in Computer Science, 1997.

    Google Scholar 

  12. D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the ACM, 2(5):323–342, April 1983.

    Google Scholar 

  13. J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. LICS’ 90, 5 th IEEE Int. Symp. on Logic in Computer Science, 1990.

    Google Scholar 

  14. G’erard C’ec’e, Alain Finkel, and S. Purushothaman Iyer. Unreliable channels are easier to verify than perfect channels. Information and Computation, 124(1):20–31, 10 January 1996.

    Google Scholar 

  15. A. Choquet and A. Finkel. Simulation of linear FIFO nets having a structured set of terminal markings. In Proc. 8 th European Workshop on Applications and Theory of Petri Nets, 1987.

    Google Scholar 

  16. E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specification. ACM Trans. on Programming Languages and Systems, 8(2):244–263, April 1986.

    Google Scholar 

  17. G. Delzanno, J. Esparza, and A. Podelski. Constraint-based analysis of broadcast protocols. In Proc. CSL’99, 1999.

    Google Scholar 

  18. E.A. Emerson and K.S. Namjoshi. On model checking for non-deterministic infinite-state systems. In Proc. LICS’ 98 13 th IEEE Int. Symp. on Logic in Computer Science, pages 70–80, 1998.

    Google Scholar 

  19. J. Esparza, A. Finkel, and R. Mayr. On the verification of broadcast protocols. In Proc. LICS’ 99 14 th IEEE Int. Symp. on Logic in Computer Science, 1999.

    Google Scholar 

  20. A. Finkel. Reduction and covering of infinite reachability trees. Information and Computation, 89:144–179, 1990.

    Article  MATH  MathSciNet  Google Scholar 

  21. A. Finkel. Decidability of the termination problem for completely specified protocols. Distributed Computing, 7(3), 1994.

    Google Scholar 

  22. A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere. Technical Report LSV-98-4, Ecole Normale Sup’erieure de Cachan, April 1998.

    Google Scholar 

  23. M. Gouda. Closed covers: to verify progress for communicating finite state machines. IEEE Trans. on Software Engineering, SE-10(6):846–855, Nov. 1984.

    Google Scholar 

  24. M.G. Gouda, E.M. Gurari, T.-H. Lai, and L.E. Rosier. On deadlock detection in systems of communicating finite state machines. Computers and Artificial Intelligence, 6(3):209–228, 1987.

    MATH  Google Scholar 

  25. G.J. Holzmann. The model checker SPIN. IEEE Trans. on Software Engineering, SE-23(5):279–295, May 1997.

    Google Scholar 

  26. R.M. Karp and R.E. Miller. Parallel program schemata. Journal of Computer and Systems Sciences, 3(2):147–195, May 1969.

    Google Scholar 

  27. K.G. Larsen, P. Pettersson, and W. Yi. Uppaal in a nutshell. Software Tools for Technology Transfer, 1(1–2), 1997.

    Google Scholar 

  28. G. LeLann. Distributed systems-towards a formal approach. In B. Gilchrist, editor, IFIP77, pages 155–160. North-Holland, 1977.

    Google Scholar 

  29. R. Mayr. Undecidable problems in unreliable computations. In Theoretical Informatics (LATIN’2000), number 1776 in Lecture Notes in Computer Science, 2000.

    Chapter  Google Scholar 

  30. J.K. Pachl. Protocol description and analysis based on a state transition model with channel expressions. In Protocol Specification, Testing, and Verification VII, May 1987.

    Google Scholar 

  31. W. Peng and S. Purushothaman. Data flow analysis of communicating finite state machines. ACM Trans. on Programming Languages and Systems, 13(3):399–442, July 1991.

    Google Scholar 

  32. J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in cesar. In 5th International Symposium on Programming, Turin, volume 137 of LNCS, pages 337–352. Springer Verlag, 1982.

    Google Scholar 

  33. H. Rudin, West, and P. Zafiropulo. Automated protocol validation-one chain of development. In Proc. Computer Network Protocols Symposium Liege, 1978.

    Google Scholar 

  34. A.P. Sistla and L.D. Zuck. Automatic temporal verification of buffer systems. In Larsen and Skou, editors, Proc. Workshop on Computer Aided Verification, volume 575 of LNCS. Springer Verlag, 1991.

    Google Scholar 

  35. M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. LICS’ 86, 1st IEEE Int. Symp. on Logic in Computer Science, pages 332–344, June 1986.

    Google Scholar 

  36. C.H. West. Automated validation of a communications protocol: the ccitt x.21 recommendation. IBM Journal on Research and Development, 22(1), Jan. 1978.

    Google Scholar 

  37. Pierre Wolper. Expressing interesting properties of programs in propositional temporal logic (extended abstract). In Proc. 13th ACM Symp. on Principles of Programming Languages, pages 184–193, Jan. 1986.

    Google Scholar 

  38. Pierre Wolper and Bernard Boigelot. Verifying systems with infinite but regular state spaces. In Proc. 10th Int. Conf. on Computer Aided Verification, volume 1427 of LNCS, pages 88–97, Vancouver, July 1998. Springer Verlag.

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computer Systems, P.O. Box 325, S-751 05, Uppsala, Sweden

    Parosh Aziz Abdulla & Bengt Jonsson

Authors
  1. Parosh Aziz Abdulla
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bengt Jonsson
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, BRICS, Aalborg University, Fredrik Bajersvej 7, 9220, Aalborg, Denmark

    Kim G. Larsen

  2. BRICS, Aarhus University, Ny Munkegade, Bldg. 540, 8000, Aarhus C, Denmark

    Mogens Nielsen

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Abdulla, P.A., Jonsson, B. (2001). Channel Representations in Protocol Verification. In: Larsen, K.G., Nielsen, M. (eds) CONCUR 2001 — Concurrency Theory. CONCUR 2001. Lecture Notes in Computer Science, vol 2154. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44685-0_1

Download citation

  • DOI: https://doi.org/10.1007/3-540-44685-0_1

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42497-0

  • Online ISBN: 978-3-540-44685-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation