Abstract
The communicating sequential processes (CSP) proposed by Hoare are a model for parallel computation in which the processes do not share a variable and perform the interprocess information exchange and synchronization by the communication instruction function. This paper first extends the verification system for the partial validity of CSP previously proposed by the authors and an axiomatic system is presented by implementing part of the inference rules which can deal with the deadlock‐free property of CSP. The soundness of the system is shown. The system previously proposed by the authors can provide the inferences in a concurrent way independently of the processes, without following the sequential procedure of proving a property for a process and proving a certain relation between processes. The system proposed in this paper employs a similar procedure and verification is made in parallel for the partial validity and deadlock‐free property of CSP.
| Original language | English |
|---|---|
| Pages (from-to) | 1-10 |
| Number of pages | 10 |
| Journal | Systems and Computers in Japan |
| Volume | 18 |
| Issue number | 4 |
| DOIs | |
| Publication status | Published - Jan 1 1987 |
| Externally published | Yes |
Fingerprint
ASJC Scopus subject areas
- Theoretical Computer Science
- Information Systems
- Hardware and Architecture
- Computational Theory and Mathematics
Cite this
Verification system for freedom from deadlock of communicating sequential processes. / Murakami, Masaki; Inagaki, Yasuyoshi.
In: Systems and Computers in Japan, Vol. 18, No. 4, 01.01.1987, p. 1-10.Research output: Contribution to journal › Article
}
TY - JOUR
T1 - Verification system for freedom from deadlock of communicating sequential processes
AU - Murakami, Masaki
AU - Inagaki, Yasuyoshi
PY - 1987/1/1
Y1 - 1987/1/1
N2 - The communicating sequential processes (CSP) proposed by Hoare are a model for parallel computation in which the processes do not share a variable and perform the interprocess information exchange and synchronization by the communication instruction function. This paper first extends the verification system for the partial validity of CSP previously proposed by the authors and an axiomatic system is presented by implementing part of the inference rules which can deal with the deadlock‐free property of CSP. The soundness of the system is shown. The system previously proposed by the authors can provide the inferences in a concurrent way independently of the processes, without following the sequential procedure of proving a property for a process and proving a certain relation between processes. The system proposed in this paper employs a similar procedure and verification is made in parallel for the partial validity and deadlock‐free property of CSP.
AB - The communicating sequential processes (CSP) proposed by Hoare are a model for parallel computation in which the processes do not share a variable and perform the interprocess information exchange and synchronization by the communication instruction function. This paper first extends the verification system for the partial validity of CSP previously proposed by the authors and an axiomatic system is presented by implementing part of the inference rules which can deal with the deadlock‐free property of CSP. The soundness of the system is shown. The system previously proposed by the authors can provide the inferences in a concurrent way independently of the processes, without following the sequential procedure of proving a property for a process and proving a certain relation between processes. The system proposed in this paper employs a similar procedure and verification is made in parallel for the partial validity and deadlock‐free property of CSP.
UR - http://www.scopus.com/inward/record.url?scp=0023327388&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0023327388&partnerID=8YFLogxK
U2 - 10.1002/scj.4690180401
DO - 10.1002/scj.4690180401
M3 - Article
AN - SCOPUS:0023327388
VL - 18
SP - 1
EP - 10
JO - Systems and Computers in Japan
JF - Systems and Computers in Japan
SN - 0882-1666
IS - 4
ER -