{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,22]],"date-time":"2023-10-22T20:45:11Z","timestamp":1698007511231},"reference-count":9,"publisher":"Wiley","issue":"4","license":[{"start":{"date-parts":[[2007,3,21]],"date-time":"2007-03-21T00:00:00Z","timestamp":1174435200000},"content-version":"vor","delay-in-days":7384,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Systems &amp; Computers in Japan"],"published-print":{"date-parts":[[1987,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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\u2010free 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\u2010free property of CSP.<\/jats:p>","DOI":"10.1002\/scj.4690180401","type":"journal-article","created":{"date-parts":[[2007,7,7]],"date-time":"2007-07-07T13:33:11Z","timestamp":1183815191000},"page":"1-10","source":"Crossref","is-referenced-by-count":0,"title":["Verification system for freedom from deadlock of communicating sequential processes"],"prefix":"10.1002","volume":"18","author":[{"given":"Masaki","family":"Murakami","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yasuyoshi","family":"Inagaki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2007,3,21]]},"reference":[{"key":"e_1_2_1_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/357103.357110"},{"key":"e_1_2_1_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/828.833"},{"key":"e_1_2_1_4_2","doi-asserted-by":"crossref","unstructured":"T.ElradandN.Francez.A weakest precondition semantics for communicating sequential processes IBM Research Report RC9773 (1982).","DOI":"10.1007\/3-540-11494-7_7"},{"key":"e_1_2_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_2_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289266"},{"key":"e_1_2_1_7_2","article-title":"Kripke semantics of interprocess communication system","volume":"184","author":"Murakami M.","year":"1985","journal-title":"I. E. C. E., Japan"},{"issue":"11","key":"e_1_2_1_8_2","first-page":"1846","article-title":"Verification system for partial validity of interprocess serial communication system","volume":"68","author":"Murakami M.","year":"1985","journal-title":"Trans. I. E. C. E., Japan"},{"key":"e_1_2_1_9_2","first-page":"11","volume-title":"Parallel process description language occum, bit","author":"Onai R.","year":"1984"},{"key":"e_1_2_1_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/1780.1805"}],"container-title":["Systems and Computers in Japan"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fscj.4690180401","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/scj.4690180401","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,21]],"date-time":"2023-10-21T06:39:51Z","timestamp":1697870391000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/scj.4690180401"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1987,1]]},"references-count":9,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1987,1]]}},"alternative-id":["10.1002\/scj.4690180401"],"URL":"https:\/\/doi.org\/10.1002\/scj.4690180401","archive":["Portico"],"relation":{},"ISSN":["0882-1666","1520-684X"],"issn-type":[{"value":"0882-1666","type":"print"},{"value":"1520-684X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1987,1]]}}}