This paper presents proof rules for port-directed communication and broadcast. The proof method is an extension of the proof technique proposed by Misra and Chandy in which input/output sequences are used to describe the state of a process or a subsystem. Various examples are presented to illustrate the use of the proof technique.
This is a preview of subscription content, log in to check access.
Buy single article
Instant access to the full article PDF.
Price includes VAT for USA
Subscribe to journal
Immediate online access to all issues from 2019. Subscription will auto renew annually.
This is the net price. Taxes to be calculated in checkout.
A. Silberschatz, Port-directed communication,Computer Journal,24:1 (1981).
Jin, Zhiquan, Communication and Broadcast in Concurrent Programming, to be published.
C. A. R. Hoare, Communicating sequential processes,C.ACM,21:8 (1978).
C. M. Levin and D. Gries, A proof technique for communicating sequential processes,Acta Inform., 15 (1981).
J. Misra and K. Mani Chandy, Proofs of networks of processes,IEEE Trans. on Software Engineering, SE-7:4(1981).
C. A. R. Hoare, A model for communicating sequential processes, Comput. Lab., Oxford Univ., Dec. 1978.
K. R. Apt, N. Francez and W.P. de Roever, A proof system for communicating sequential processes,TOPLAS, 2 (1980).
S. Owicki and D. Gries, An axiomatic proof technique for parallel programs,Acta Inform., 6 (1976).
C. A. R. Hoare, An axiomatic basis for computer programmingC. ACM,21:8 (1978).
Jin Zhiquan and A. Silberschatz, Port-directed broadcast, in Proc. 1985 Conf. on Information Sciences and Systems, March (1985).
About this article
Cite this article
Jin, Z., Silberschatz, A. Proof techniques for port-directed communication and broadcast. J. of Comput. Sci. & Technol. 2, 81–91 (1987). https://doi.org/10.1007/BF02973486
- Inference Rule
- Output Port
- Input Port
- Proof Technique
- Proof Method