Proofs of Networks of Processes
- 1 July 1981
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering
- Vol. SE-7 (4) , 417-426
- https://doi.org/10.1109/tse.1981.230844
Abstract
We present a proof method for networks of processes in which component processes communicate exclusively through messages. We show how to construct proofs of invariant properties which hold at all times during network computation, and terminal properties which hold upon termination of network computation, if network computation terminates. The proof method is based upon specifying a process by a pair of assertions, analogous to pre-and post-conditions in sequential program proving. The correctness of network specification is proven by applying inference rules to the specifications of component processes. Several examples are proved using this technique.Keywords
This publication has 10 references indexed in Scilit:
- A Correctness Proof for Communicating Processes: A Small ExercisePublished by Springer Nature ,1982
- A Proof System for Communicating Sequential ProcessesACM Transactions on Programming Languages and Systems, 1980
- A simple model of distributed programs based on implementation-hiding and process autonomyACM SIGPLAN Notices, 1980
- Principles of proving concurrent programs in GypsyPublished by Association for Computing Machinery (ACM) ,1979
- Communicating sequential processesCommunications of the ACM, 1978
- Formal verification of parallel programsCommunications of the ACM, 1976
- Proving monitorsCommunications of the ACM, 1976
- An axiomatic proof technique for parallel programs IActa Informatica, 1976
- Program proving: CoroutinesActa Informatica, 1973
- An axiomatic basis for computer programmingCommunications of the ACM, 1969