Abstract
Protocol verification detects the existence of logic errors in protocol design specifications. Various verification approaches have been proposed to deal with the state space explosion problem resulting from the reachability analysis. This paper proposes a parallel protocol verification algorithm, called the Two-Phase algorithm, in an attempt to provide a maximum of verification with a minimum of state space. This algorithm allows verification for all FSMs to be executed in parallel through exploring fewer states. To quantify the reduction in state space, the paper provides the state space complexity comparison between the reachability analysis and the Two-Phase algorithm. The paper defines four protocol models giving the lower and upper bound state space complexity according to both state and channel synchronization characteristics of protocols. For each model, the state space complexity of these two verification algorithms are analyzed and compared. The Two-Phase algorithm is shown to require much smaller state space. To support the analytical result, this paper also gives experimental results on several protocols, including the Call Set-Up and Termination phases of the CCITT X.25 and X.75 protocols.
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
G. V. Bochmann, "Finite State Description of Communication Protocols," Computer Networks, Vol. 2, Oct. 1978, pp. 361–372.
G. V. Bochmann and C. A. Sunshine, "Formal Methods in Communication Protocol Design," IEEE Trans. on Communications, Vol. COM-28, No. 4, April 1980, pp. 624–631.
D. Brand and P. Zafiropulo, "On Communicating Finite-State Machines," Journal of the ACM, Vol 30, No. 2, April 1983, pp. 323–342.
A. Danthine, "Protocol Representation with Finite State Models," IEEE Trans. on Communications, Vol. COM-28, No. 4, April 1980, pp. 632–643.
M. G. Gouda, "Closed Covers: To Verify Progress of Communicating Finite State Machines," IEEE Trans. on Software Engineering, Nov. 1984, Vol. SE-10, No. 6, pp. 846–855.
Y. Kakuda, Y. Wakahara, and M. Norigoe, "A New Algorithm For Fast Protocol Validation," Proc. IEEE COMPSAC, 1986, pp. 228–236.
S. Lam and A. Shankar, "Protocol Verification via Projections," IEEE Trans. on Software Engineering, Vol. SE-10, No. 4, July 1984, pp. 325–342.
F. Lin, P. Chu, and M. Liu, "Protocol Verification Using Reachability Analysis: The State Space Explosion Problem and Relief Strategies," Proc. ACM SIGCOMM, Aug. 1987.
N. F. Maxemchuk and K. Sabnani, "Probabilistic Verification of Communication Protocols," Protocol Specification, Testing, and Verification, VII, pp. 307–320, North-Holland, 1987.
P. M. Merlin, "Specification and Validation of Protocols," IEEE Trans. on Communications, Vol. COM-27, No. 11, Nov. 1979, pp. 1671–1680.
"Communication Protocol Modeling," Edited by Carl A. Sunshine, Artech House.
S. T. Vuong and D. D. Cowan, "A Decomposition Method for the Validation of Structured Protocols," Proc. IEEE INFOCOM, April 1982.
S. T. Vuong, D. D. Hui, and D. D. Cowan, "VALIRA — A Tool for Protocol Validation Via Reachability Analysis," Protocol Specification, Testing, and Verification, VI. North-Holland, 1986.
M. C. Yuang, "Survey of Protocol Verification Techniques Based on Finite State Machine Models," Proc. NBS Computer Networking Symposium, 1988, pp. 164–172.
M. C. Yuang and A. Kershenbaum, "Parallel Protocol Verification Using the Localized Approach: A Two-Phase Algorithm,” Proc. Ninth International Symposium on Protocol Specification, Testing, and Verification, 1989.
P. Zafiropulo, "Protocol Validation by Duologue-Matrix Analysis," IEEE Trans. Commun. COM-26, 8(August, 1978), pp. 1187–1194.
P. Zafiropulo, et al., "Towards Analyzing and Synthesizing Protocols," IEEE Trans. on Communications, COM-28, 4(April, 1980), pp. 651–661.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yuang, M.C., Kershenbaum, A. (1990). Parallel protocol verification: The two-phase algorithm and complexity analysis. In: Sifakis, J. (eds) Automatic Verification Methods for Finite State Systems. CAV 1989. Lecture Notes in Computer Science, vol 407. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52148-8_26
Download citation
DOI: https://doi.org/10.1007/3-540-52148-8_26
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52148-8
Online ISBN: 978-3-540-46905-6
eBook Packages: Springer Book Archive