Specification and verification of liveness properties of cyclic, concurrent processes
- 1 January 1988
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 10 (1) , 156-177
- https://doi.org/10.1145/42192.42195
Abstract
A technique is described for software specification and verification of concurrent, distributed systems. The complete specification of a program is given in terms of a hierarchical structure of module specifications. Module external specifications are abstract; module internal specifications are descriptions of internal implementations, either in terms of submodules or actual code. The verification that an implementation satisfies its specification is language independent for the former and language dependent for the latter. Distinguishing the liveness properites provided by a module and the liveness properties required by a module (from its comodules) allows the specification and verification of a given module to be independent from the specification and verification of its comodules.Keywords
This publication has 16 references indexed in Scilit:
- The ``Hoare Logic'' of CSP, and All ThatACM Transactions on Programming Languages and Systems, 1984
- Specifying Concurrent Program ModulesACM Transactions on Programming Languages and Systems, 1983
- Modular verification of concurrent programsPublished by Association for Computing Machinery (ACM) ,1982
- A proof technique for communicating sequential processesActa Informatica, 1981
- A Proof System for Communicating Sequential ProcessesACM Transactions on Programming Languages and Systems, 1980
- The ?Hoare logic? of concurrent programsActa Informatica, 1980
- Communicating sequential processesCommunications of the ACM, 1978
- A proof method for cyclic programsActa Informatica, 1978
- Proving assertions about parallel programsJournal of Computer and System Sciences, 1975
- Assigning meanings to programsPublished by American Mathematical Society (AMS) ,1967