A formalism for specifying communicating processes

ABSTRACT

We present a framework to specify and validate the design of message passing systems with synchronous or asynchronous communications. Our approach allows users to represent concurrent systems in a novel language and to justify the design automatically using the simulator. The method handles safety and deadlock properties. Concurrent systems are specified in an operational manner by transition systems. This tool is built for analyzing the logical consistency of communicating processes, specifically systolic-arrays and communication protocols. We describe how a systolic array and a communication protocol can be specified and justified with respect to its design.

REFERENCES

• 1: G. Boudol, R. de Simone, and D. Vergamini, Experiment with Auto and Autograph on a Simple Case Sliding Window Protocol, TR-870, Inria, July 1988.
• 2: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 3: Rance Cleaveland , Joachim Parrow , Bernhard Steffen, A Semantics Based Verification Tool for Finite State Systems, Proceedings of the IFIP WG6.1 Ninth International Symposium on Protocol Specification, Testing and Verification IX, p.287-302, June 06-09, 1989
• 4: Edsger W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, v.18 n.8, p.453-457, Aug. 1975 [doi>10.1145/360933.360975]
• 5: J.C. Godskesen, K. G. Larsen, and M. Zeeberg, TAV User Manual, Proceeding of Workshop on A aromatic Verification Methods for Finite State Systems, Grenoble, 1989.
• 6: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 7: Gerard J. Holzmann, Design and validation of computer protocols, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 8: Donald E. Knuth, Additional comments on a problem in concurrent programming control, Communications of the ACM, v.9 n.5, p.321-322, May 1966 [doi>10.1145/355592.365595]
• 9: H.T. Kung and C. E. Leiserson, "Systolic Arrays (for VLSI)," Sparse Matrix Syrup., SIAM, 1978.
• 10: Leslie Lamport, The mutual exclusion problem: part I—a theory of interprocess communication, Journal of the ACM (JACM), v.33 n.2, p.313-326, April 1986 [doi>10.1145/5383.5384]
• 11: F. Lin, T. Shih, and N. Ling "Axiomatic Approach for Systolic Array Design," Proceeding of the Logic Programming Conference 91, Tokyo, Japan, July 8-11, 1991.
• 12: Fuyau Lin , Timothy K. Shih, Verification of Systolic Architecture Designs, Proceedings of the 4th International PARLE Conference on Parallel Architectures and Languages Europe, p.381-396, June 15-18, 1992
• 13: R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 14: James L. Peterson , Abraham Silberschatz, Operating system concepts (2nd ed.), Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1985
• 15: Jean-Luc Richier , Carlos Rodriguez , Joseph Sifakis , Jacques Voiron, Verification in XESAR of the Sliding Window Protocol, Proceedings of the IFIP WG6.1 Seventh International Conference on Protocol Specification, Testing and Verification VII, p.235-248, May 05-08, 1987
• 16: J. M. Spivey, Understanding Z, A Specification Language and its Formal Semantics, D.phil Thesis, Oxford University Computing Laboratory, 11 Keble Road, Oxford, UK, October 1985.
• 17: A. S. Tanenbaum, Computer networks, Prentice-Hall, Inc., Upper Saddle River, NJ, 1988

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.2 Modes of Computation
          Subjects: Parallelism and concurrency

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming

          Nouns: CSP
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

  I. Computing Methodologies
  I.6 SIMULATION AND MODELING
      I.6.8 Types of Simulation
          Subjects: Parallel

General Terms:
Algorithms, Design, Languages, Verification