×
Nguyen, Van; Demers, Alan; Gries, David; Owicki, Susan

A model and temporal proof system for networks of processes. (English) Zbl 0598.68025

Distrib. Comput. 1, 7-25 (1986).
An approach is presented for modeling networks of processes that communicate exclusively through message passing. A process (or a network) is defined by its set of possible behaviors, where each behavior is an abstraction of an infinite execution sequence of the process. The resulting model is simple and modular and facilitates information hiding. It can describe both synchronous and asynchronous networks. It supports recursively-defined networks and can characterize liveness properties such as progress of inputs and outputs, termination, and deadlock.
A sound and complete temporal proof system based on the model is presented. It is compositional - a specification of a network is formed naturally from specifications of its components.

Cited in 6 Documents

MSC:

68N25 Theory of operating systems

Keywords:

message passing; infinite execution sequence; synchronous and asynchronous networks; liveness properties; termination; deadlock
PDF BibTeX XML Cite
\textit{V. Nguyen} et al., Distrib. Comput. 1, 7--25 (1986; Zbl 0598.68025)
Full Text: DOI
  • logo of hbz
  • logo of WorldCat

References:

[1] Apt KR (1981) Ten years of Hoare’s logic: a survey – Part 1. ACM TOPLAS 3:431–483 · Zbl 0471.68006
[2] Barringer H, Kuiper R, Pnueli A (1984) Now you may compose temporal logic specifications. Proc 16th ACM Symp. Theor Comput
[3] Brock JD, Ackerman WB (1981) Scenarios: a model of nondeterminate computation. International Colloquium on Formalization of Programming Concepts
[4] Brookes SD (1984) A semantics and proof system for communicating processes. Lect Notes Comput Sci 164:68–85
[5] Chen ZC, Hoare CAR (1981) Partial correctness of communicating processes and protocols. Technical monograph PRG-20, Programming Research Group, Oxford University Computing Laboratory
[6] Hewitt C, Baker HG (1977) Laws for communicating parallel processes. Proc IFIP 77:987–992 · Zbl 0363.68077
[7] Hoare CAR (1983) Notes on communicating sequential processes. Technical Monograph PRG-33, Programming Research Group, Oxford University Computing Laboratory
[8] Kahn G (1974) The semantics of a simple language for parallel programming. Inf Process pp 471–475 · Zbl 0299.68007
[9] Kahn G, MacQueen DB (1977) Coroutines and networks of parallel processes. Proc IFIP 77:993–998 · Zbl 0363.68076
[10] Lamport L (1983) What good is temporal logic? Proc IFIP 83:657–668
[11] Levin GM, Gries D (1981) A proof technique for communicating sequential processes. Acta Inf 15:281–302 · Zbl 0463.68034
[12] Manna Z. Pnueli A (1981a) Verification of concurrent programs, Part 1: The temporal framework. Tech Rep STAN-CS-81-836, Stanford University. June 1981
[13] Manna Z. Pnueli A (1981 b) Verification of concurrent programs, Part 2: Temporal proof principles. Tech Rep STAN-CS-81-843, Stanford University. Sept 1981 · Zbl 0481.68019
[14] Manna Z, Pnueli A (1983) How to cook a temporal proof system for your pet language. Proc. 10th ACM Sym Prince of Prog Lang. Jan 1983, pp 141–154
[15] Milner R (1980) A calculus of communicating systems. Lect Notes Comput Sci 92 · Zbl 0452.68027
[16] Misra J, Chandy KM (1981) Proofs of networks of processes. IEEE Trans Soft Eng SE-7, 4 · Zbl 0468.68030
[17] Misra J, Chandy KM, Smith T (1982) Proving safety and liveness of communicating processes with examples. Proc SIGACT-SIGOPS Symp Princ of Distributed Computing, Aug 1982, pp 201–208
[18] Nguyen V (1985a) A theory of processes. Ph. D. Thesis, Department of Computer Science, Cornell University · Zbl 0940.47508
[19] Nguyen V (1985b) The incompleteness of Misra and Chandy’s proof systems. Inf Proc Lett (to appear) · Zbl 0575.68022
[20] Nguyen V, Demers A, Gries D, Owicki S (1985) Behavior: a temporal approach to process modeling. IBM Workshop on Logics of Programs. June 1985 · Zbl 0606.68022
[21] Nguyen V, Gries D, Owicki S (1985) A model and temporal proof system for networks of processes. Proc 12th ACM Symp Princ of Prog Lang. Jan 1985, pp 121–131
[22] Pratt V (1982) On the composition of processes. Proc 9th ACM Symp Princ of Prog Lang. Jan 1982, pp 213–223
[23] Shapiro E, Takeuchi A (1983) Object-oriented programming in Concurrent Prolog. J New Generation Comput 1:25–48
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.