Article

Free access

Verification of communication protocols using data flow analysis

Authors:

Gleb N. Naumovich,

Lori A. Clarke,

Leon J. OsterweilAuthors Info & Claims

SIGSOFT '96: Proceedings of the 4th ACM SIGSOFT symposium on Foundations of software engineering

Pages 93 - 105

https://doi.org/10.1145/239098.239114

Published: 01 October 1996 Publication History

Abstract

In this paper we demonstrate the effectiveness of data flow analysis for verifying requirements of communication protocols. Data flow analysis is a static analysis method for increasing confidence in the correctness of software systems by automatically verifying that a given software artifact (e.g., design or code) must behave consistently with a specified requirement. In this case study, we apply the FLAVERS data flow analysis tool to pseudocode designs of the three way handshake connection establishment protocol and of the alternating bit protocol and prove that the behavior of the pseudocode is consistent with protocol behavioral requirement specifications. We show how FLAVERS is a particularly effective because it is computationally inexpensive, requires minimal human interaction, and is a general approach that can be applied incrementally until the desired accuracy is achieved. In addition, we show how assumptions about the environment in which a software system is executed can be incorporated into the analysis, using message losses as an example. We present experimental results and derive some guidelines about the classes of protocol requirement specifications that may be amenable to verification using FLAVERS.

References

[1]

W. Richards Adrion, M.A. Branstad, and J.C. Cherniavski. Validation, Verification, and Testing of Computer Software. ACM Computing Surveys, 14(2):159- 192, June 1982.

Digital Library

[2]

George S. Avrunin, Ugo A. Buy, James C. Corbett, Laura K. Dillon, and Jack C. Wileden. Automated Analysis of Concurrent Systems with the Constrained Expression Toolset. IEEE Transactions on Software Engineering, 17(11):1204-1222, November 1991.

Digital Library

[3]

T. Bolognesi and E. Brinksma. Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems, North-Holland, 14:25-59, 1987,

Digital Library

[4]

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 Fifth Annual IEEE Symposium on Logic in Computer Science, pages 428-439, 1990.

[5]

S. Budkowski and P. Dembinski. An introduction to Estelle: A specification language for distributed systems. Computer Networks and ISDN Systems, North-Holland, 14:3-23, 1987.

Digital Library

[6]

F. Belina and D. Hogrefe. The CCITT-specification and description language SDL. Computer Networks and ISDN Systems, 16, 4:311-341, 1989.

Digital Library

[7]

Naser Barghouti, Nihal Nounou, and Yechiam Yemini. An integrated protocol development environment. Proc. 6th int. symp. on protocol specification, testing and verification, June 10-13, 1986, 1986.

[8]

Gregor Bochmann and Alexandre Petrenko. Protocol testing: Review of methods and relevance for software testing. In Proc. 1994 International Symposium on Software Testing and Analysis, August 1994.

Digital Library

[9]

K. A. Bartlett, R. A. Scantlebury, and P. T. Wilkinson. A note on reliable full-duplex transmission over half-duplex lines. Comm. of the ACM, 12(5):260-265, 1969.

Digital Library

[10]

R. Castanet, A. Dupeux, and P. Guitton. Ada, a well suited language for specification and implementation of protocols. Proc. 5th int. symp. on protocol specification, testing and uerification, June 10-13, 1985, 1985.

Digital Library

[11]

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, April 1986.

Digital Library

[12]

G~rard C~C~, Alain Finkel, and S. Purishothaman Iyer. Duplication, insertion and lossiness errors in unreliable communication. In Proc. of the Second ACM SIGSOFT Symposium on Foundations of Software Engineering, December 1994.

Digital Library

[13]

James C. Corbett. Verifying General Safety and Liveness Properties with Integer Programming. In Proceedings of the Fourth Workshop on Computer Aided Verification, pages 337-348, 1992.

Digital Library

[14]

Matthew Dwyer and Lori Clarke. Data Flow Analysis for Verifying Properties of Concurrent Programs, In ACM SIGSOFT'94 Software Engineering Notes, Proceedings of the Second ACM Sigsoft Symposium on Foundations of Software Engineering, v. 19, n, 5, pages 62-75, December 1994.

Digital Library

[15]

Matthew Dwyer. Data Flow Analysis for Verifying Correctness Properties of Concurrent Programs. PhD thesis, University of Msssachussetts, Amherst, 1995.

Digital Library

[16]

Patrice Godefroid and Pierre Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. In Proceedings of the Third Workshop on Computer Aided Verification, pages 417-428, July 1991.

Digital Library

[17]

M.S. Hecht. Flow Analysis of Computer Programs. North-Holland, New York, 1977.

Digital Library

[18]

G. J. Holzmann, P. Godefroid, and D, Pirottin. Coverage preserving reduction strategies for reachability analysis. In Proc. 12th Int. Conf on Protocol Specification, Testing, and Verification, INWG/IFIP, Orlando, Fl., June 1992.

Digital Library

[19]

C.A.R. Hoare. An Axiomatic Basis of Computer Programming. Communications of the ACM, 12(10):576-583, October 1969.

Digital Library

[20]

Gerard J. Holzmann. On limits and possibilities of automated protocol analysis. Protowl Specification, Testing and Verification VII, IFIP 1987, pages 339- 344, 1987.

Digital Library

[21]

Gerard J. Holzmann. Design and Validation of Computer Protowls. Prentice Hall Software Series, 1991.

Digital Library

[22]

W. E. Howden and G. M. Shi. Linear and structural event sequence analysis. In Proceedings of the 1996 international Symposium on Software Testing and Analysis (ISSTA), pages 98-106, 1996.

Digital Library

[23]

James F. Kurose and Yechiam Yemini. The specification and verification of a connection establishment protocol using temporal logic. Proc. 2nd int. work. shop on protocol specification, testing and verifica-tion, May 17-20, 1982.

Digital Library

[24]

Robin Milner. A Calculus of Communicating Systems, Lecture Notes in Computer Science, Vol.92. Springer-Verlag, Berlin, 1980. Appeared as vol. 92, Lecture Notes in Computer Science.

Digital Library

[25]

T. J. Marlowe and B. G. Ryder. Properties of Data Flow Frameworks. Acts Informatica, (28):121-163, 1990.

Digital Library

[26]

S.P. Masticola and B.G. Ryder. A Model of Ada Programs for Static Deadlock Detection in Polynomial Time. In Proceedings of the Workshop on Pamllel and Distributed Debugging, pages 97-107. ACM, May 1991.

Digital Library

[27]

Kurt M. Olender and Leon J. Osterweil. Cecil: A Sequencing Constraint Language for Automatic Static Analysis Generation. IEEE Transactions on Software Engineering, 16(3) :268-280, March 1990.

Digital Library

[28]

Jan Paehl. Protocol description and analysis baaed on a state transition model with channel expressions. Protocol Specification, Testing and Verification VII, IFIP 1987, pages 207-219, 1987.

Digital Library

[29]

Amir Pnueli. The Temporal Logic of Programs. In Proceedings of the Eighteenth Symposium on Foundations of Computer Science, Providence, 1977, pages 46-57, 1977.

[30]

J. L. Rlchier, C. Rodriguez, J. Sifakis, and J. Voiron. Verification in Xesar of the sliding window protocol. Protocol Specification, Testing and Verification VII, IFIP 1987, pages 235-248, 1987.

Digital Library

[31]

J. Reif and S. Smolka. The Complexity of Reachability in Distributed Communicating Processes. Acts Informatica, 25(3):333-354, 1988.

Digital Library

[32]

John H. Reif and Scott A. Smolka. Data flow analysis of distributed communicating processes. International Journal of Parallel Progmmming, 19(1), 1990.

Digital Library

[33]

Deepinder P. Sidhu and Ting-Kau Leung. Formal methods for protocol testing: A detailed study. IEEE Transactions on Software Engineering, 15(4):413- 426, April 1989.

Digital Library

[34]

J. M. Spivey. The Z Notation A Reference Manual. Prentice Hall, International Series in Computer Science, 1992.

Digital Library

[35]

Krishan Sabnani and Mischa Schwartz. Verification of a multidestination protocol using temporal logic. Proc. 2nd int. workshop on protocol specification, testing and verification, May 17-20, 1982.

Digital Library

[36]

Richard N. Taylor. Complexity of Analyzing the Synchronization Structure of Concurrent Programs. Acts Informatica, 19:57-84, 1983.

Digital Library

[37]

Richard N. Taylor and L. J. Osterweil. Anomaly Detection in Concurrent Software by Static Data Flow Analysis. IEEE tinsactions on Software Engineering, 6(3):265-278, May 1980.

[38]

A. Valmari. A Stubborn Attack on State Explosion. In Edmund M. Clarke and R.P. Kurshan, editors, Computer-Aided Verification 90, pages 25- 41. American Mathematical Society, Providence RI, 1991. Number 3 in DIMACS Series in Discrete Mathematics and Theoretical Computer Science.

Digital Library

[39]

Son T. Vuong, Daniel D. Hui, and Don D. Cowan. Valira - a tool for protocol validation via reachability analysis. Proc. 6th int. symp. on protocol specification, testing and verification, June 10-13, 1986, 1986.

[40]

Larry Yelowitz, Susan Gerhart, and G. Hilborn. Modeling a network protocol in affirm and ada. Proc. 2nd int. workshop on protocol specification, testing and verification, May 17-20, 1982, 1982.

Digital Library

[41]

V. Yodaiken and Krithi Ramamritham. Verification of a Reliable Net Protocol. In Formal Techniques in Real-Time and Fault-Tolerent Systems, Lecture Notes in Computer Science No. 571, pages 193-215. Springer-Verlag, 1992.

Cited By

Roozbehani MMegretski AFeron E(2013)Optimization of Lyapunov Invariants in Verification of Software SystemsIEEE Transactions on Automatic Control10.1109/TAC.2013.224147258:3(696-711)Online publication date: Mar-2013
https://doi.org/10.1109/TAC.2013.2241472
Udrea OLumezanu CFoster J(2008)Rule-based static analysis of network protocol implementationsInformation and Computation10.1016/j.ic.2007.05.007206:2-4(130-157)Online publication date: 1-Feb-2008
https://dl.acm.org/doi/10.1016/j.ic.2007.05.007
Sobeih AViswanathan MMarinov DHou J(2007)J-Sim: An Integrated Environment for Simulation and Model Checking of Network Protocols2007 IEEE International Parallel and Distributed Processing Symposium10.1109/IPDPS.2007.370519(1-6)Online publication date: Mar-2007
https://doi.org/10.1109/IPDPS.2007.370519
Show More Cited By

Recommendations

Verification of communication protocols using data flow analysis

In this paper we demonstrate the effectiveness of data flow analysis for verifying requirements of communication protocols. Data flow analysis is a static analysis method for increasing confidence in the correctness of software systems by automatically ...
Analyzing encryption protocols using formal verification techniques

An approach to analyzing encryption protocols using machine-aided formal verification techniques is presented. The properties that the protocol should preserve are expressed as state invariants, and the theorems that must be proved to guarantee that the ...
Formal specification and verification of communication protocols using automated tools
ICECCS '95: Proceedings of the 1st International Conference on Engineering of Complex Computer Systems

The paper compares and contrasts various methods presently available for specification, validation and verification, with emphasis on verification. We describe an application of formal methods to protocol specification, validation, and verification, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SIGSOFT '96: Proceedings of the 4th ACM SIGSOFT symposium on Foundations of software engineering

October 1996

190 pages

ISBN:0897917979

DOI:10.1145/239098

Chairmen:
Mark Moriconi
SRI International, Menlo Park, CA
,
Gregory Abowd
Georgia Institute of Technology, Atlanta
,
Editor:
David Garlan
Carnegie Mellon Univ., Pittsburgh, PA

ACM SIGSOFT Software Engineering Notes Volume 21, Issue 6
Nov. 1996
192 pages
ISSN:0163-5948
DOI:10.1145/250707
Editor:
David Garlan
Issue’s Table of Contents

Copyright © 1996 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]

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 October 1996

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

SOFT96

Sponsor:

SIGSOFT

SOFT96: SIGSOFT '96

October 16 - 18, 1996

California, San Francisco, USA

Acceptance Rates

Overall Acceptance Rate 17 of 128 submissions, 13%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

23
Total Citations
View Citations
701
Total Downloads

Downloads (Last 12 months)72
Downloads (Last 6 weeks)14

Reflects downloads up to 27 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Roozbehani MMegretski AFeron E(2013)Optimization of Lyapunov Invariants in Verification of Software SystemsIEEE Transactions on Automatic Control10.1109/TAC.2013.224147258:3(696-711)Online publication date: Mar-2013
https://doi.org/10.1109/TAC.2013.2241472
Udrea OLumezanu CFoster J(2008)Rule-based static analysis of network protocol implementationsInformation and Computation10.1016/j.ic.2007.05.007206:2-4(130-157)Online publication date: 1-Feb-2008
https://dl.acm.org/doi/10.1016/j.ic.2007.05.007
Sobeih AViswanathan MMarinov DHou J(2007)J-Sim: An Integrated Environment for Simulation and Model Checking of Network Protocols2007 IEEE International Parallel and Distributed Processing Symposium10.1109/IPDPS.2007.370519(1-6)Online publication date: Mar-2007
https://doi.org/10.1109/IPDPS.2007.370519
Sobeih AViswanathan MMarinov DHou J(2005)Finding bugs in network protocols using simulation code and protocol-specific heuristicsProceedings of the 7th international conference on Formal Methods and Software Engineering10.1007/11576280_17(235-250)Online publication date: 1-Nov-2005
https://dl.acm.org/doi/10.1007/11576280_17
Dwyer MClarke LCobleigh JNaumovich G(2004)Flow analysis for verifying properties of concurrent software systemsACM Transactions on Software Engineering and Methodology10.1145/1040291.104029213:4(359-430)Online publication date: 1-Oct-2004
https://dl.acm.org/doi/10.1145/1040291.1040292
Atkinson D(2004)Accurate Call Graph Extraction of Programs with Function Pointers Using Type SignaturesProceedings of the 11th Asia-Pacific Software Engineering Conference10.1109/APSEC.2004.16(326-335)Online publication date: 30-Nov-2004
https://dl.acm.org/doi/10.1109/APSEC.2004.16
Cobleigh JClarke LOsterweil LMüller H(2001)The right algorithm at the right timeProceedings of the 23rd International Conference on Software Engineering10.5555/381473.381477(37-46)Online publication date: 1-Jul-2001
https://dl.acm.org/doi/10.5555/381473.381477
Atkinson DGriswold W(2001)Implementation Techniques for Efficient Data-Flow Analysis of Large ProgramsProceedings of the IEEE International Conference on Software Maintenance (ICSM'01)10.1109/ICSM.2001.972711Online publication date: 7-Nov-2001
https://dl.acm.org/doi/10.1109/ICSM.2001.972711
Cobleigh JClarke LOstenveil L(2001)The right algorithm at the right time: comparing data flow analysis algorithms for finite state verificationProceedings of the 23rd International Conference on Software Engineering. ICSE 200110.1109/ICSE.2001.919079(37-46)Online publication date: 2001
https://doi.org/10.1109/ICSE.2001.919079
Dwyer MPĂsĂreanu C(2001)Model Checking Generic Container ImplementationsGeneric Programming10.1007/3-540-39953-4_13(162-177)Online publication date: 28-Sep-2001
https://doi.org/10.1007/3-540-39953-4_13
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 Table of Contents