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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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.
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.
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.
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.
Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. Information and Computation, 127(2):91–101, 1996.
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.
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.
T.P. Blumer and D.P. Sidhu. Mechanical verification of communication protocols. IEEE Trans. on Software Engineering, SE-12(8):827–843, Aug. 1986.
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.
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.
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.
D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the ACM, 2(5):323–342, April 1983.
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.
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.
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.
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.
G. Delzanno, J. Esparza, and A. Podelski. Constraint-based analysis of broadcast protocols. In Proc. CSL’99, 1999.
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.
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.
A. Finkel. Reduction and covering of infinite reachability trees. Information and Computation, 89:144–179, 1990.
A. Finkel. Decidability of the termination problem for completely specified protocols. Distributed Computing, 7(3), 1994.
A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere. Technical Report LSV-98-4, Ecole Normale Sup’erieure de Cachan, April 1998.
M. Gouda. Closed covers: to verify progress for communicating finite state machines. IEEE Trans. on Software Engineering, SE-10(6):846–855, Nov. 1984.
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.
G.J. Holzmann. The model checker SPIN. IEEE Trans. on Software Engineering, SE-23(5):279–295, May 1997.
R.M. Karp and R.E. Miller. Parallel program schemata. Journal of Computer and Systems Sciences, 3(2):147–195, May 1969.
K.G. Larsen, P. Pettersson, and W. Yi. Uppaal in a nutshell. Software Tools for Technology Transfer, 1(1–2), 1997.
G. LeLann. Distributed systems-towards a formal approach. In B. Gilchrist, editor, IFIP77, pages 155–160. North-Holland, 1977.
R. Mayr. Undecidable problems in unreliable computations. In Theoretical Informatics (LATIN’2000), number 1776 in Lecture Notes in Computer Science, 2000.
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.
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.
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.
H. Rudin, West, and P. Zafiropulo. Automated protocol validation-one chain of development. In Proc. Computer Network Protocols Symposium Liege, 1978.
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.
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.
C.H. West. Automated validation of a communications protocol: the ccitt x.21 recommendation. IBM Journal on Research and Development, 22(1), Jan. 1978.
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.
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.
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
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