Verification system for freedom from deadlock of communicating sequential processes

Masaki Murakami, Yasuyoshi Inagaki

Research output: Contribution to journalArticle

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

Fingerprint

Deadlock
Synchronization
Communication
Partial
Sequential Procedure
Inference Rules
Parallel Computation
Soundness
Concurrent

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 journalArticle

@article{bb1ef8b2eda748768c26ea6d42e1f39a,
title = "Verification system for freedom from deadlock of communicating sequential processes",
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.",
author = "Masaki Murakami and Yasuyoshi Inagaki",
year = "1987",
month = "1",
day = "1",
doi = "10.1002/scj.4690180401",
language = "English",
volume = "18",
pages = "1--10",
journal = "Systems and Computers in Japan",
issn = "0882-1666",
publisher = "John Wiley and Sons Inc.",
number = "4",

}

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 -