Conformity analysis for communication protocols

ABSTRACT

In this paper we propose a methodology for conformity analysis of communication protocols. By conformity analysis it is meant to demonstrate that a protocol does indeed provide the service for which it is intended. We specify both a protocol and its service by a CSP (Communicating Sequential Processes) based language. To perform the conformity analysis we develop a transformation system to extract from a CSP process the communication sequences that may arise during its execution, and to express these sequences in terms of behavior expressions in CCS (Calculus of Communicating Systems). By performing algebraic manipulations and the equivalence proof on these expressions, we can show that the external behavior of a protocol conforms to its intended service. A version of the Alternating Bit Protocol is used to demonstrate the feasibility of the methodology.

REFERENCES

• 1: Krzysztof R. Apt , Nissim Francez , Willem P. de Roever, A Proof System for Communicating Sequential Processes, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.3, p.359-385, July 1980 [doi>10.1145/357103.357110]
• 2: Gregor V. Bochmann, Communication protocols and error recovery procedures, Proceedings of the 1975 ACM SIGCOMM/SIGOPS workshop on Interprocess communications, p.45-50, January 1975
• 3: Day, J. D., and Zimmermann H. "The OSI Reference Model" Proceedings of the IEEE 71(12) : 1334-1340, June 1983,
• 4: Hennessy, M., Li, W., and P{otkin, G. "A First Attempt at Translating CSP into CCS". Proc. 2nd international Conference on Distributed Computing Systems, pp. 105-115, April 1981.
• 5: , Hennessy, M. "An Introduction to a Calculus of Communicating Systems" In New Advances in Distributed Computer Systems, K.G. Beauchamp (ed.), D. Reidel Publishing Company, 1982, pp. 245-262.
• 6: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 7: C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
• 8: ISO. Information Processing Systems - Open Systems Interconnection - LOTOS - A Formal Description Technique based on the Temporal Ordering of Observational Behavior, {SO/DP 8807, March 1985.
• 9: Levin. G. M., and Gries, D. "A Proof Technique for Communicating Sequential Processes". .4cta inf 15:281-302, 1981.
• 10: Liu, N. C. and Liu, M. T. "CSP-based Specifications for Network Protocols and Services". {EEE Computer Networking Symposium : 95-102, December 1984.
• 11: R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 12: H. Partsch , R. Steinbrüggen, Program Transformation Systems, ACM Computing Surveys (CSUR), v.15 n.3, p.199-236, Sept. 1983 [doi>10.1145/356914.356917]
• 13: Schwartz, R. L. and Me{liar-Smith. P. M. "From State Machines to Temporal Logic: Specification Methods for Protocol Standards". IEEE Trans. on Communications COiW-30(12} : 2486-2496, December 1982.
• 14: N. Soundararajan, Axiomatic semantics of communicating sequential processes, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.4, p.647-662, Oct. 1984 [doi>10.1145/1780.1805]
• 15: Tenney, R. L. "One Formal Description Technique For {SO OSI". Proceedings of the International Conference on Communications, pp.1296-1300, June 1983.

INDEX TERMS

Classification:
  C. Computer Systems Organization
  C.1 PROCESSOR ARCHITECTURES
  C.2 COMPUTER-COMMUNICATION NETWORKS

  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming

          Nouns: CSP
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: CSP
      D.3.3 Language Constructs and Features

          Nouns: CSP

General Terms:
Experimentation, Languages, Performance, Standardization, Verification