Abstract
We consider symbolic on-the-fly verification methods for systems of finite-state machines that communicate by exchanging messages via unbounded and lossy FIFO queues. We propose a novel representation formalism, called simple regular expressions (SREs), for representing sets of states of protocols with lossy FIFO channels. We show that the class of languages representable by SREs is exactly the class of downward closed languages that arise in the analysis of such protocols. We give methods for (i) computing inclusion between SREs, (ii) an SRE representing the set of states reachable by executing a single transition in a system, and (iii) an SRE representing the set of states reachable by an arbitrary number of executions of a control loop of a program. All these operations are rather simple and can be carried out in polynomial time. With these techniques, one can construct a semi-algorithm which explores the set of reachable states of a protocol, in order to check various safety properties.
Chapter PDF
References
Parosh Aziz Abdulla and Bengt Jonsson. Undecidable verification problems for programs with unreliable channels. Inform. and Comput., 130(1):71–90, 1996.
Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. Inform. and Comput., 127(2):91–101, 1996.
B. Boigelot and P. Godefroid. Symbolic verification of communication protocols with infinite state spaces using QDDs. In CAV'96, LNCS 1102.
B. Boigelot, P. Godefroid, B. Willems, and P. Wolper. The power of QDDs. Available at http://www.montefiore.ulg.ac.be/~biogelot/research/BGWW97.ps.
B. Boigelot, P. Godefroid, B. Willems, and P. Wolper. The power of QDDs. In SAS'97, LNCS 1997.
A. Bouajjani and P. Habermehl. Symbolic reachability analysis of fifo-channel systems with nonregular sets of configurations. http://www.imag.fr/VERIMAG/PEOPLE/Peter.Habermehl.
A. Bouajjani and P. Habermehl. Symbolic reachability analysis of fifo-channel systems with nonregular sets of configurations. In ICALP '97, LNCS 1256. 1997.
G. V. Bochman. Finite state description of communicating protocols. Computer Networks, 2:361–371, 1978.
B. Boigelot and P. Wolper. Symbolic verification with periodic sets. In CAV'94, LNCS 818. 1994.
D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the ACM, 2(5):323–342, April 1983.
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.
Gérard Céé, Alain Finkel, and S. Purushothaman Iyer. Unreliable channels are easier to verify than perfect channels. Inform. and Comput., 124(1):20–31, 10 January 1996.
C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. In CAV'90.
A. Finkel and O. Marcé. Verification of infinite regular communicating automata. Technical report, LIFAC, ENS de Cachan, 1996. Tech. Rep.
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. Higman. Ordering by divisibility in abstract algebras. Proc. London Math. Soc., 2:326–336, 1952.
G.J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.
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.
A.P. Sistla and L.D. Zuck. Automatic temporal verification of buffer systems. In Larsen and Skou, editors, CAV'91, LNCS 575. 1991.
M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In LICS'86, IEEE, 1986.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abdulla, P.A., Bouajjani, A., Jonsson, B. (1998). On-the-fly analysis of systems with unbounded, lossy FIFO channels. In: Hu, A.J., Vardi, M.Y. (eds) Computer Aided Verification. CAV 1998. Lecture Notes in Computer Science, vol 1427. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028754
Download citation
DOI: https://doi.org/10.1007/BFb0028754
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64608-2
Online ISBN: 978-3-540-69339-0
eBook Packages: Springer Book Archive