Extensions to communicating sequential processes to allow protocol performance specification

ABSTRACT

Formalisms based on Hoare's Communicating Sequential Processes (CSP) and Milner's Calculus of Communicating Systems (CCS) for verifying protocols are currently being used by the International Standard Organisation (ISO). However, these models need to be extended if protocol performance specification and verification is to be done, as neither of these models have timing information (other than sequencing) nor a way of specifying controlled loss of information. This paper presents two extensions to Hoare's CSP that are felt by the author to provide suitable mechanisms for specifying protocol performance. Firstly, the effects of introducing time into CSP are presented, based on the work done by Reed and Roscoe. Secondly, the traces model is modified by associating probabilities with event sequences. Finally, some example specifications are given using these two extensions.

REFERENCES

• 1: Home, C.A.R. "Communicating Sequential Processes'', Prentice-HaU International series in Computer Science, Prentice-Hall International, UK, 1985
• 2: R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 3: L. Logrippo , D. Simon , H. Ural, Executable description of the OSI transport service in Prolog, Proc. of IFIP WG 6.1 4th Int'l Workshop on Protocol specification, testing, and verification, IV, p.279-293, June 1985, Skytop Lodge, Pennsylvania, United States
• 4: G M Reed , A W Roscoe, A timed model for communicating sequential processes, International Colloquium on Automata, Languages and Programming on Automata, languages and programming, p.314-323, September 1986, Rennes, France
• 5: Zic, J.J., "A New Communication Protocol Specification and Analysis Technique", Technical Report TR287, July 1986, Basser Department of Computer Science, University of Sydney
• 6: Azaria Paz, Introduction to probabilistic automata (Computer science and applied mathematics), Academic Press, Inc., Orlando, FL, 1971
• 7: Bergstra, J.A., Klop, J.W., Olderog, E.-R. "Failures without Chaos: A New Process Semantics for Fair Abstraction", Report CS-R8625, August 1986, Centmm voor Wiskunde en Informatica (CWI), Amsterdam
• 8: Zic, J.J., "Stochastic Determinism as an Extension to Communicating Sequential Processes", Technical Report TR306, May 1987, Basser Department of Computer Science, University of Sydney (Submitted for publication).
• 9: E.-R. Olderog, Specification-oriented programming in TCSP, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• 10: C B Jones, Systematic software development using VDM, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1986
• 11: Morris, K. comment in an Honours seminar, Basser Department of Computer Science, University of Sydney, May 1983.

INDEX TERMS

Primary Classification:
  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS

Additional Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS

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

          Nouns: CSP

General Terms:
Performance, Standardization, Theory, Verification