Proving safety and liveness of communicating processes with examples

ABSTRACT

A method is proposed for reasoning about safety and liveness properties of message passing networks. The method is hierarchical and is based upon combining the specifications of component processes to obtain the specification of a network. The inference rules for safety properties use induction on the number of messages transmitted; liveness proofs use techniques similar to termination proofs in sequential programs. We illustrate the method with two examples: concatenations of buffers to construct larger buffers and a special case of Stenning protocol for message communication over noisy channels.

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: Brent Tzion Hailpern, Verifying concurrent processes using temporal logic, 1980
• 3: Hailpern, B. and S. Owicki, "Modular Verification of Computer Communication Protocols," Research Report RC8726, IBM Watson Research Center, March 1981.
• 4: Levin, G.M. and D. Gries, "A Proof System for Communicating Sequential Processes," Acta Informatica 15, Springer-Verlag, 1981.
• 5: Misra, J. and K.M. Chandy, "Proofs of Networks of Processes," IEEE-TSE, Vol. SE-7, No. 4, July 1981.
• 6: Martin John Ossefort, A unified approach to formal verification of network safety properties, 1982
• 7: Owicki, S. and L. Lamport, "Proving Liveness Properties of Concurrent Programs," Computer Systems Laboratory, Stanford University, 1980.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
          Subjects: Protocol verification

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

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

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Algorithms, Languages, Performance, Verification

Keywords:
Communicating processes, Liveness, Message-passing systems, Proofs of process networks, Safety