The Library
Specification and verification of total correctness of distributed programs
Tools
Tools
Tools
Joseph, Mathai and Pandya, Paritosh K. (1987) Specification and verification of total correctness of distributed programs. Coventry, UK: University of Warwick. Department of Computer Science. (Department of Computer Science Research Report). (Unpublished)
|
PDF
WRAP_cs-rr-096.pdf - Requires a PDF viewer. Download (16Mb) | Preview |
Abstract
This paper describes a compositional specification and proof system for networks of distributed processes. Each process in a network is specified using first order logic in terms of a presupposition P and an affirmation A as a triple (P) S (A). For purely sequential programs, these triples reduce to the familiar Hoare triples extended for total correctness. In distributed programs, P-A triples allow the Internal behaviour of a process to be specified in the context of the communications of the other processes in the network. Communications may either by synchronous or asynchronous. Properties such as termination, the absence of deadlock and the absence of livelock can be verified. As the technique is syntax-directed and allows network abstraction, proofs follow the structure of the program and a subnetwork within a network can be replaced by a single process. It also allows proof of the properties of non-terminating processes, such as servers.
| Item Type: | Report | ||||
|---|---|---|---|---|---|
| Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||
| Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||
| Library of Congress Subject Headings (LCSH): | Electronic data processing -- Distributed processing | ||||
| Series Name: | Department of Computer Science Research Report | ||||
| Publisher: | University of Warwick. Department of Computer Science | ||||
| Place of Publication: | Coventry, UK | ||||
| Official Date: | February 1987 | ||||
| Dates: |
|
||||
| Number: | Number 96 | ||||
| Number of Pages: | 19 | ||||
| DOI: | CS-RR-096 | ||||
| Institution: | University of Warwick | ||||
| Theses Department: | Department of Computer Science | ||||
| Status: | Not Peer Reviewed | ||||
| Publication Status: | Unpublished | ||||
| Reuse Statement (publisher, data, author rights): | P. Pandya and M. Joseph, “P-A logic: A Compositional Proof System for Distributed Programs”, <i>Distributed Computing</i> <b>5</b>, pp. 37-54 (1991) | ||||
| Related URLs: |
Request changes or add full text files to a record
Repository staff actions (login required)
 |
View Item |
Downloads
Downloads per month over past year
