Verification system for freedom from deadlock of communicating sequential processes

Masaki Murakami, Yasuyoshi Inagaki

Research output: Contribution to journalArticlepeer-review


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 languageEnglish
Pages (from-to)1-10
Number of pages10
JournalSystems and Computers in Japan
Issue number4
Publication statusPublished - 1987
Externally publishedYes

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Information Systems
  • Hardware and Architecture
  • Computational Theory and Mathematics


Dive into the research topics of 'Verification system for freedom from deadlock of communicating sequential processes'. Together they form a unique fingerprint.

Cite this