Copyright and Licensing
Articles accepted for publication will be licensed under the Creative Commons BY-NC-SA. Authors must sign a non-exclusive distribution agreement after article acceptance.
Reasoning about Protocols using Dijkstra’s Calculus
Keywords:
weakest precondition, correctness, guarded process, non- deterministic selection, protocol, weakest cooperationAbstract
A mathematical model for the specification and verification of a data link layer protocol is proposed. The weakest precondition calculus, developed by Dijkstra, originally for sequential programs, has been chosen for this purpose. It is demonstrated that the wp-calculus provides a basis, not only for the modeling but also, for a straightforward and thorough analysis of large and complex distributed systems like data link layer protocol. This analysis contributes to the understanding of the system and could lead to an improvement in the design. The technique has been illustrated by describing the sliding window protocol.
Downloads
Download data is not yet available.
References
[1] J. A. Hall, Seven myths of formal methods, IEEE Software, vol. 7, September 1990, pp. 11–19.
[2] E. W. Dijkstra, A discipline of programming, Prentice Hall, 1976.
[3] M. Ben-Ari, Mathematical Logic for Computer Science, Prentice Hall, 1993.
[4] David S. Rosenblum, Specifying concurrent systems with TSL, IEEE Software, 8(3), May 1991, pp. 52-61.
[5] Yoshinao Isobe and Kazuhito Ohmaki, A process logic for distributed system synthesis, Proc. APSEC 2000, IEEE 7th Asia–Pacific Software Engineering Conference, 2000, pp. 62-69.
[6] A. K. Singh, Ph. D. Thesis, Faculty of Engineering and Technology, Jadavpur University, Kolkata, India, May 2003.
[7] Peter G. Neumann, Distributed systems have distributed risks, Communications of the ACM, 39(11), Nov 1996, Page 130.
[8] Peter G. Neumann, Using formal methods to reduce risks, Communications of the ACM, 39(7), Jul 1996, Page 114.
[9] D. Harel and A. Pnuali, On the development of reactive systems, In K. R. Apt, editor, Logics and Models of Concurrent Systems, vol. F-13 of NATO ASI Series, Springer-Verlag, 1985, pp. 477-498.
[10] Panagiotis Manolios and Richard Trefler, Safety and liveness in branching time, Proc. IEEE 16th Annual Symposium on Logic in Computer Science, 2001, pp. 366-374.
[11] Orna Kupferman and Moshe Y. Vardi, Synthesizing distributed systems, Proc. IEEE 16th Annual Symposium on Logic in Computer Science, 2001, pp. 389-398.
[12] A. K. Bandyopadhyay and J Bandyopadhyay, On the derivation of a correct deadlock free communication kernel for loop connected message passing architecture from its user's specification, Journal of System Architecture, vol. 46, No. 13, 2000, pp. 1257–1261.
[13] K. M. Chandi and B. A. Sanders, Predicate transformers for reasoning about concurrent computation, Science of Computer Programming, vol. 24, 1995, pp. 129–148.
[14] A. K. Bandyopadhyay, A mathematical model for the specification of data link layer protocols, In Proc. COMNAM-2000, December, 2000, pp. 109–114.
[15] A. S. Tanenbaum, Computer Networks 3/e, Prentice Hall of India, 1998.
[16] Z. Manna and A. Pnueli, Temporal Verification of Reactive Systems: Safety, Springer-Verlag, New York, 1995.
[17] Peter B. Ladkin, Using the temporal logic of actions: A tutorial on TLA verification, Technical Report RVS-RR-97-08, RVS group, Universitat Bielefeld, Technische Fakultat, June 1997. Available through http://www.rvs.uni-bielefeld.de
[18] Leslie Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems, vol. 16, No. 3, pp. 872–923, May 1994.
[19] Dirk Henkel, Safely sliding windows, Technical Report RVS-RR-97-05a & 05b, RVS group, Uuniversitat Bielefeld, Technische Fakultat, May 1997.
[20] Dirk Henkel, Safely sliding windows: Into the depths of formal system verification, Research Report, RVS group, Faculty of Technology, University of Bielefeld, April 1999. Available through http://www.rvs.uni-bielefeld.de
[21] Martin Abadi, Leslie Lamport, The existence of refinement mappings, Theoretical Computer Science, 82(2):253-284, May 1991.
[22] Abdelillah Mokkedem, Michael J. Ferguson, and Robert deB. Johnston, A TLA solution to the specification and verification of the RLP1 retransmission protocol, In Proc. Formal Methods Europe Symposium, September 1997.
[23] A. K. Singh and A. K. Bandyopadhyay, A mathematical model for the specification of sliding window protocol, In Proc. CIIC-2001, December 2001, pp. 585–587
[2] E. W. Dijkstra, A discipline of programming, Prentice Hall, 1976.
[3] M. Ben-Ari, Mathematical Logic for Computer Science, Prentice Hall, 1993.
[4] David S. Rosenblum, Specifying concurrent systems with TSL, IEEE Software, 8(3), May 1991, pp. 52-61.
[5] Yoshinao Isobe and Kazuhito Ohmaki, A process logic for distributed system synthesis, Proc. APSEC 2000, IEEE 7th Asia–Pacific Software Engineering Conference, 2000, pp. 62-69.
[6] A. K. Singh, Ph. D. Thesis, Faculty of Engineering and Technology, Jadavpur University, Kolkata, India, May 2003.
[7] Peter G. Neumann, Distributed systems have distributed risks, Communications of the ACM, 39(11), Nov 1996, Page 130.
[8] Peter G. Neumann, Using formal methods to reduce risks, Communications of the ACM, 39(7), Jul 1996, Page 114.
[9] D. Harel and A. Pnuali, On the development of reactive systems, In K. R. Apt, editor, Logics and Models of Concurrent Systems, vol. F-13 of NATO ASI Series, Springer-Verlag, 1985, pp. 477-498.
[10] Panagiotis Manolios and Richard Trefler, Safety and liveness in branching time, Proc. IEEE 16th Annual Symposium on Logic in Computer Science, 2001, pp. 366-374.
[11] Orna Kupferman and Moshe Y. Vardi, Synthesizing distributed systems, Proc. IEEE 16th Annual Symposium on Logic in Computer Science, 2001, pp. 389-398.
[12] A. K. Bandyopadhyay and J Bandyopadhyay, On the derivation of a correct deadlock free communication kernel for loop connected message passing architecture from its user's specification, Journal of System Architecture, vol. 46, No. 13, 2000, pp. 1257–1261.
[13] K. M. Chandi and B. A. Sanders, Predicate transformers for reasoning about concurrent computation, Science of Computer Programming, vol. 24, 1995, pp. 129–148.
[14] A. K. Bandyopadhyay, A mathematical model for the specification of data link layer protocols, In Proc. COMNAM-2000, December, 2000, pp. 109–114.
[15] A. S. Tanenbaum, Computer Networks 3/e, Prentice Hall of India, 1998.
[16] Z. Manna and A. Pnueli, Temporal Verification of Reactive Systems: Safety, Springer-Verlag, New York, 1995.
[17] Peter B. Ladkin, Using the temporal logic of actions: A tutorial on TLA verification, Technical Report RVS-RR-97-08, RVS group, Universitat Bielefeld, Technische Fakultat, June 1997. Available through http://www.rvs.uni-bielefeld.de
[18] Leslie Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems, vol. 16, No. 3, pp. 872–923, May 1994.
[19] Dirk Henkel, Safely sliding windows, Technical Report RVS-RR-97-05a & 05b, RVS group, Uuniversitat Bielefeld, Technische Fakultat, May 1997.
[20] Dirk Henkel, Safely sliding windows: Into the depths of formal system verification, Research Report, RVS group, Faculty of Technology, University of Bielefeld, April 1999. Available through http://www.rvs.uni-bielefeld.de
[21] Martin Abadi, Leslie Lamport, The existence of refinement mappings, Theoretical Computer Science, 82(2):253-284, May 1991.
[22] Abdelillah Mokkedem, Michael J. Ferguson, and Robert deB. Johnston, A TLA solution to the specification and verification of the RLP1 retransmission protocol, In Proc. Formal Methods Europe Symposium, September 1997.
[23] A. K. Singh and A. K. Bandyopadhyay, A mathematical model for the specification of sliding window protocol, In Proc. CIIC-2001, December 2001, pp. 585–587
Downloads
Published
2004-04-01
Issue
Section
Original Articles
License
How to Cite
[1]
“Reasoning about Protocols using Dijkstra’s Calculus”, JCS&T, vol. 4, no. 01, pp. p. 26–31, Apr. 2004, Accessed: Jan. 17, 2026. [Online]. Available: https://journal.info.unlp.edu.ar/JCST/article/view/910
