article

Free access

Protocol verification using reachability analysis: the state space explosion problem and relief strategies

Authors:

M. T. LiuAuthors Info & Claims

ACM SIGCOMM Computer Communication Review, Volume 17, Issue 5

Pages 126 - 135

https://doi.org/10.1145/55483.55496

Published: 01 August 1987 Publication History

Abstract

Reachability analysis has proved to be one of the most effective methods in verifying correctness of communication protocols based on the state transition model. Consequently, many protocol verification tools have been built based on the method of reachability analysis. Nevertheless, it is also well known that state space explosion is the most severe limitation to the applicability of this method. Although researchers in the field have proposed various strategies to relieve this intricate problem when building the tools, a survey and evaluation of these strategies has not been done in the literature. In searching for an appropriate approach to tackling such a problem for a grammar-based validation tool, we have collected and evaluated these relief strategies, and have decided to develop our own from yet another but more systematic approach. The results of our research are now reported in this paper. Essentially, the paper is to serve two purposes: first, to give a survey and evaluation of existing relief strategies; second, to propose a new strategy, called PROVAT (PROtocol VAlidation Testing), which is inspired by the heuristic search techniques in Artificial Intelligence. Preliminary results of incorporating the PROVAT strategy into our validation tool are reviewed in the paper. These results show the empirical evidence of the effectiveness of the PROVAT strategy.

References

[1]

J. -P. Ansart. Issues and Tools for Protocol Specification. The Advanced Course on Distributed Systems- Methods and Tools for Specification. Springer-Verlag, 1985, pages 481-538.

Digital Library

[2]

A. Gardner. Search. The Handbook of Artificial Intelligence. William Kaufman, 1981, Chapter 1I.

[3]

T.P. Blumer and D. P. Sidhu. Mechanical VeriFmation and Automatic Implementation of Communication Protocols. IEEE Trans. on Software Engineering SE-12(8):827-843, August, 1986.

Digital Library

[4]

D. Brand and P. Zafiropulo. On Communicating Finite-State Machines. Journal of A CM 30(2):323-342, April, 1983.

Digital Library

[5]

T.Y. Choi and R. E. Miller. A Decomposition Method for the Analysis and Design of Finite State Protocols. In Proe. Data Communication Symposium, pages 167-176. ACM SIGCOMM, t983.

Digital Library

[6]

C. Chow, M. G. Gouda, and S. S. Larn. A Discipline for Constructing Multiphase Communication Protocols. ACM Trans. on Computer Systems 3(4):315-343. November, 1985.

Digital Library

[7]

M.G. Gouda and Y. T. Yu. Protocol Validation by Maximal Progress State Exploration. IEEE Trans. on Communications COM-32(1):94-97, Janunary, 1984.

[8]

M.G. Gouda and J.-Y. Han. Protocol Validation by Fair Progress State Exploration. Computer Networks and ISDN Systems 9:353-361, 1985.

[9]

G.J. Holzmann. Tracing Protocol. AT~T Technical Journal 64(10):2413-2433, December, 1985.

[10]

G.J. Holzmann. Automatic Protocol Validation in Argos: Assertion Proving and Scatter Searching. IEEE Trans. on Software Enqineerinq SE-13(6):683-696, June, 1987.

Digital Library

[11]

E. Horowitz and S. Sahni. Chapter 6. Fundamentals of Computer Algorithms. Computer Science Press, 1978, pages 318.

Digital Library

[12]

M. I~oh and H. Ichikawa. Protocol Verification Algorithm Using Reduced Reachability Analysis. The Trans. on the IECE of Japan E66(2):88-93, February, 1983.

[13]

Y. Kakuda, Y. Wakahara, and M. Norigoe. A New Algorithm for Fast Protocol Validation. In Proc. COMPSAC, pages 228-236. {EEE, 1986.

[14]

S.S. Lam and A. U. Shanker. Protocol Verification via Projections. IEEEE Trans. on Software Engineering SE-10(4):325-342, July, 1984.

Digital Library

[15]

F.J. Lin, P. M. Chu, and M. T. Liu. Probabilistic Transmission Grammmar. I987 Unpublished Notes.

[16]

c.s. L~. Automated Validation o{ Communication Protocols. PhD thesis, The Ohio State Univ., 1986.

[17]

J. Peral. Heuristics -- Intelligent Search Strategies for Computer Problem Solving. Addison-Wesley, 1984.

Digital Library

[18]

S. Purushotkaman and P. A. Subrahmanyam. Reasoning About Probabilistic Behavior in Concurrent Systems. IEEEE Trans. on Software Engineerino SE-13(6):740-745, June, 1087.

Digital Library

[19]

J. Rubin and C. H. West. An Improved Protocol Validation Technique. Computer Networks 6:65-73, 1982.

[20]

A.Y. Teng and M. T. Liu. The Transmission Grammar Model for Protocol Construction. {n Proc. Trends and Applications Symposium, pages 110-120. NBS~ 1980.

[21]

L.D. Umbaugh. Automated Techniques for Specification and Validation of Communication Protocols. PhD thesis, The Ohio Sate Univ., 1983.

Digital Library

[22]

S.T. Vuong and D. D. Cowan. A Decomposition Method for the Validation of Structured Protocols. In Proc. {NFOCOM, pages 209-220. IEEE, 1982.

[23]

S.T. Vuong, D. D. tiui, and D. D. Cowan. VALIRA- A Tool for Protocol Validation Via Reachability Analysis. Protocol Specification, Testing, and Verificatior~, North-Holland, 1987, pages 35-41.

[24]

C.H. West and P. Zafiropulo. Automated Validation of a Communication Protocol: the CCITT X.21 Recommendation. IBM dourr~al of Research and Development 22(1):60-71, 1978.

[25]

c.H. West. Applications and Limitations of Automated Protocol Validation. Protocol Specification, Testing, and Verification, II. North-Holland, 1982, pages 361-371.

Digital Library

[26]

C.H. West. Protocol Validation by Random State Exploration. Protocol Specification, Testing, and Verification, VI. North-Holland, t987, pages 233-242.

[27]

P. Zafiropulo, C. H. West, ~. Rudin, D. D. Cowan, and D. Brand. Towards Analyzing and Synthesizing Protocols. IEEE Trans. on Communication 28(4):651-660, April, 1980.

[28]

J.-R. Zhao and G. V. Bochmann. Reduced Reachability Analysis of Communicaiton Protocols : A New Approach. Protocol Specification, Testing, and Verification, VI. North-Holland, 1987. pages 243-254.

Cited By

Moormann LGoorden Mvan de Mortel-Fronczak JFokkink WMaessen PRooda J(2020)Efficient Validation of Supervisory Controllers using Symmetry ReductionIFAC-PapersOnLine10.1016/j.ifacol.2021.04.07453:4(288-295)Online publication date: 2020
https://doi.org/10.1016/j.ifacol.2021.04.074
Anjaria K(2020)Negation and Entropy: Effectual Knowledge Management Equipment for Learning OrganizationsExpert Systems with Applications10.1016/j.eswa.2020.113497(113497)Online publication date: May-2020
https://doi.org/10.1016/j.eswa.2020.113497
Yasrebi MRafe Vparvin HNejatian S(2019)An efficient approach to state space management in model checking of complex software systems using machine learning techniquesJournal of Intelligent & Fuzzy Systems10.3233/JIFS-190023(1-13)Online publication date: 29-Nov-2019
https://doi.org/10.3233/JIFS-190023
Show More Cited By

Index Terms

Protocol verification using reachability analysis: the state space explosion problem and relief strategies

Recommendations

Protocol verification using reachability analysis: the state space explosion problem and relief strategies
SIGCOMM '87: Proceedings of the ACM workshop on Frontiers in computer communications technology

Reachability analysis has proved to be one of the most effective methods in verifying correctness of communication protocols based on the state transition model. Consequently, many protocol verification tools have been built based on the method of ...
Ameliorating the State Explosion Problem
Ameliorating the state explosion problem

Comments

Information & Contributors

Information

Published In

cover image ACM SIGCOMM Computer Communication Review

ACM SIGCOMM Computer Communication Review Volume 17, Issue 5

Oct./Nov. 1987

397 pages

ISSN:0146-4833

DOI:10.1145/55483

Editor:
J. J. Garcia-Luna-Aceves
SRI International, Menlo Park, CA

Issue’s Table of Contents

SIGCOMM '87: Proceedings of the ACM workshop on Frontiers in computer communications technology
August 1987
409 pages
ISBN:0897912454
DOI:10.1145/55482
Editor:
J. J. Garcia-Luna-Aceves
SRI International, Menlo Park, CA

Copyright © 1987 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 August 1987

Published in SIGCOMM-CCR Volume 17, Issue 5

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

123
Total Citations
View Citations
1,057
Total Downloads

Downloads (Last 12 months)130
Downloads (Last 6 weeks)21

Reflects downloads up to 15 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Moormann LGoorden Mvan de Mortel-Fronczak JFokkink WMaessen PRooda J(2020)Efficient Validation of Supervisory Controllers using Symmetry ReductionIFAC-PapersOnLine10.1016/j.ifacol.2021.04.07453:4(288-295)Online publication date: 2020
https://doi.org/10.1016/j.ifacol.2021.04.074
Anjaria K(2020)Negation and Entropy: Effectual Knowledge Management Equipment for Learning OrganizationsExpert Systems with Applications10.1016/j.eswa.2020.113497(113497)Online publication date: May-2020
https://doi.org/10.1016/j.eswa.2020.113497
Yasrebi MRafe Vparvin HNejatian S(2019)An efficient approach to state space management in model checking of complex software systems using machine learning techniquesJournal of Intelligent & Fuzzy Systems10.3233/JIFS-190023(1-13)Online publication date: 29-Nov-2019
https://doi.org/10.3233/JIFS-190023
Schmidtke H(2018)A survey on verification strategies for intelligent transportation systemsJournal of Reliable Intelligent Environments10.1007/s40860-018-0070-54:4(211-224)Online publication date: 19-Oct-2018
https://doi.org/10.1007/s40860-018-0070-5
Yeh CLu HYeh JHuang S(2017)Path Exploration Based on Monte Carlo Tree Search for Symbolic Execution2017 Conference on Technologies and Applications of Artificial Intelligence (TAAI)10.1109/TAAI.2017.26(33-37)Online publication date: Dec-2017
https://doi.org/10.1109/TAAI.2017.26
Sandıkkaya MOvatman THarmancı A(2016)Design and formal verification of a cloud compliant secure logging mechanismIET Information Security10.1049/iet-ifs.2014.062510:4(203-214)Online publication date: 1-Jul-2016
https://doi.org/10.1049/iet-ifs.2014.0625
Mizouni RLazarova-Molnar S(2015)Project Schedule Simulation: Incorporating Human Factors’ Uncertainty and Features’ Priority in Task ModelingJournal of Software10.17706/jsw.10.8.939-96010:8(939-960)Online publication date: 2015
https://doi.org/10.17706/jsw.10.8.939-960
Knapik MPenczek W(2015)Fixed-Point Methods in Parametric Model CheckingIntelligent Systems'201410.1007/978-3-319-11313-5_22(231-242)Online publication date: 2015
https://doi.org/10.1007/978-3-319-11313-5_22
Groote JKouters TOsaiweran A(2015)Specification guidelines to avoid the state space explosion problemSoftware Testing, Verification & Reliability10.1002/stvr.153625:1(4-33)Online publication date: 1-Jan-2015
https://dl.acm.org/doi/10.1002/stvr.1536
Zhou KYong JWang XRen LHou GChang J(2013)Accelerating Software Model Checking Based on Program BackboneRevised Selected Papers of the 10th International Symposium on Advanced Parallel Processing Technologies - Volume 829910.1007/978-3-642-45293-2_26(347-358)Online publication date: 27-Aug-2013
https://dl.acm.org/doi/10.1007/978-3-642-45293-2_26
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents