Abstract
We study the verification of properties of communication protocols modeled by a finite set of finite-state machines that communicate by exchanging messages via unbounded FIFO queues. It is well-known that most interesting verification problems, such as deadlock detection, are undecidable for this class of systems. However, in practice, these verification problems may very well turn out to be decidable for a subclass containing most “real” protocols.
Motivated by this optimistic (and, we claim, realistic) observation, we present an algorithm that may construct a finite and exact representation of the state space of a communication protocol, even if this state space is infinite. Our algorithm performs a loop-first search in the state space of the protocol being analyzed. A loop-first search is a search technique that attempts to explore first the results of successive executions of loops in the protocol description (code). A new data structure named Queue-content Decision Diagram (QDD) is introduced for representing (possibly infinite) sets of queue-contents. Operations for manipulating QDDs during a loop-first search are presented.
A loop-first search using QDDs has been implemented, and experiments on several communication protocols with infinite state spaces have been performed. For these examples, our tool completed its search, and produced a finite symbolic representation for these infinite state
“Aspirant” (Research Assistant) for the National Fund for Scientific Research (Belgium). The work of this author was done in part while visiting Bell Laboratories.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Information and Computation, 104(1):2–34, May 1993.
P. A. Abdulla and B. Jonsson. Verifying programs with unreliable channels. In Proceedings of the 8th IEEE Symposium on Logic in Computer Science, 1993.
P. A. Abdulla and B. Jonsson. Undecidable verification problems for programs with unreliable channels. In Proc. ICALP-94, Volume 820 of Lecture Notes in Computer Science, pages 316–327. Springer-Verlag, 1994.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the 5th Symposium on Logic in Computer Science, pages 428–439, Philadelphia, June 1990.
R.E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293–318. 1992.
K. Bartlett, R. Scantlebury, and P. Wilkinson. A note on reliable full-duplex transmissions over half-duplex lines. Communications of the ACM, 2(5):260–261, 1969.
B. Boigelot and P. Wolper. Symbolic verification with periodic sets. In Proc. 6th Conference on Computer Aided Verification, Volume 818 of Lecture Notes in Computer Science, pages 55–67, Stanford, June 1994. Springer-Verlag.
D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the ACM, 2(5):323–342, 1983.
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, January 1986.
A. Choquet and A. Finkel. Simulation of linear FIFO nets having a structured set of terminal markings. In Proc. 8th European Workshop on Application and Theory of Petri Nets, pages 95–112, Saragoza, 1937.
G. Cécé, A. Finkel, and S. Purushothaman. Unreliable channels are easier to verify than perfect channels. Information and Computation, 124(3):20–31, 1996.
A. Finkel. A new class of analyzable cfsms with unbounded FIFO channels. In Proc. 8th IFIP WG 6.1 International Symposium on Protocol Specification, Testing, and Verification, pages 1–12, Atlantic City, 1988. North-Holland.
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.
P. Godefroid and D. E. Long. Symbolic Protocol Verification with Queue BDDs. In Proceedings of the 11th IEEE Symposium on Logic in Computer Science, New Brunswick, July 1996.
T. Jeron. Testing for unboundedness of FIFO channels. In Proc. STACS-91: Symposium on Theoretical Aspects of Computer Science, Volume 480 of Lecture Notes in Computer Science, pages 322–333, Hamburg, 1991. Springer-Verlag.
R. M. Karp and R. E. Miller. Parallel program schemata. Journal of Computer and System Sciences, 3(2):147–195, 1969.
M.T. Liu. Protocol engineering. Advances in Computing, 29:79–195. 1989.
H. R. Lewis and C. H. Papadimitriou. Elements of the Theory of Computation. Prentice Hall, 1981.
O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages, pages 97–107, New Orleans, January 1985.
J. K. Pachl. Protocol description and analysis based on a state transition model with channel expressions. In Proc. 7th IFIP WG 6.1 International Symposium on Protocol Specification, Testing, and Verification. North-Holland, 1987.
W. Peng and S. Purushothaman. Data flow analysis of communicating finite state machines. ACM Transactions on Programming Languages and Systems, 13(3):399–442, 1991.
J.P. Quielle and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proc. 5th Int'l Symp. on Programming, Volume 137 of Lecture Notes in Computer Science, pages 337–351. Springer-Verlag, 1981.
H. Rudin. Network protocols and tools to help produce them. Annual Review of Computer Science, 2:291–316, 1987.
L. E. Royer and H. C. Yen. Boundedness, empty channel detection and synchronization for communicating finite automata. Theoretical Computer Science, 44:69–105, 1986.
A. P. Sistla and L. D. Zuck. Automatic temporal verification of buffer systems. In Proc. 3rd Workshop on Computer Aided Verification, Volume 575 of Lecture Notes in Computer Science, pages 93–103, Aalborg, July 1991. Springer-Verlag.
A. Tanenbaum. Computer Neworks. Prentice Hall, 1989.
M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposium on Logic in Computer Science, pages 322–331, Cambridge, June 1986.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boigelot, B., Godefroid, P. (1996). Symbolic verification of communication protocols with infinite state spaces using QDDs. In: Alur, R., Henzinger, T.A. (eds) Computer Aided Verification. CAV 1996. Lecture Notes in Computer Science, vol 1102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61474-5_53
Download citation
DOI: https://doi.org/10.1007/3-540-61474-5_53
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61474-6
Online ISBN: 978-3-540-68599-9
eBook Packages: Springer Book Archive