{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,22]],"date-time":"2023-10-22T06:10:49Z","timestamp":1697955049787},"reference-count":15,"publisher":"Wiley","issue":"11","license":[{"start":{"date-parts":[[2007,3,21]],"date-time":"2007-03-21T00:00:00Z","timestamp":1174435200000},"content-version":"vor","delay-in-days":7749,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Systems &amp;amp; Computers in Japan"],"published-print":{"date-parts":[[1986,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The communication sequential processes (CSP) system proposed by Hoare is a model for parallel computation which has no shared variables and performs information exchange and synchronization among processes by means of communication commands. In this paper we first consider a set of states for the given CSP program. Using a binary relation on the set, we introduce a semantics representing only the input\u2010output relations of the CSP program. Based on this semantics, we propose an axiom system which serves to verify the partial correctness of CSP. We prove the soundness of this axiom system. The axiom system proposed in this paper differs from the previously proposed systems in the following aspects. In our system, the inferences proceed simultaneously over all processes. On the other hand, conventional methods adopt a procedure wherein a given property is first proved independently for each process and it is then shown that a certain condition holds among the processes. Our method of proof is a more direct representation of the actual execution of process.<\/jats:p>","DOI":"10.1002\/scj.4690171102","type":"journal-article","created":{"date-parts":[[2007,7,7]],"date-time":"2007-07-07T10:51:43Z","timestamp":1183805503000},"page":"11-20","source":"Crossref","is-referenced-by-count":1,"title":["Verification system for partial correctness of communicating sequential processes"],"prefix":"10.1002","volume":"17","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\/322358.322372"},{"key":"e_1_2_1_4_2","unstructured":"S. D.Brookes. A Model for Communicating Sequential Processes D. Phil. dissertation Oxford Univ. Oxford England (1983)."},{"key":"e_1_2_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/828.833"},{"key":"e_1_2_1_6_2","doi-asserted-by":"crossref","unstructured":"T.ElradandN.Francez. A weakest precondition Semantics for Communicating Sequential Processes IBM Research Report (1982).","DOI":"10.1007\/3-540-11494-7_7"},{"key":"e_1_2_1_7_2","volume-title":"Semantics of Non\u2010determinism, concurrency and communication","author":"Francez N.","year":"1979"},{"key":"e_1_2_1_8_2","doi-asserted-by":"crossref","unstructured":"N. D.Francez Lehmann andA.Pnueli. A linear history semantics for distributed language: extended abstract Proc. of FOCS ACM (1980).","DOI":"10.1109\/SFCS.1980.5"},{"key":"e_1_2_1_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09237-4"},{"key":"e_1_2_1_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_2_1_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289266"},{"key":"e_1_2_1_12_2","doi-asserted-by":"crossref","unstructured":"Z.MannaandA.Pnueli. How to cook a temporal proof system for your pet language Proc. of Symp. on POPL ACM (1983).","DOI":"10.1145\/567067.567082"},{"key":"e_1_2_1_13_2","first-page":"53","article-title":"Kripke\u2010type semantics of communicating sequential processes","volume":"84","author":"Murakami M.","year":"1985","journal-title":"Papers of Technical Group on Automata and Languages, I.E.C.E., Japan"},{"key":"e_1_2_1_14_2","first-page":"11","volume-title":"Bit","author":"Onai","year":"1984"},{"key":"e_1_2_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/1780.1805"},{"key":"e_1_2_1_16_2","volume-title":"Parallel Programming \u2010 A Bibliography","author":"Bell D. H.","year":"1983"}],"container-title":["Systems and Computers in Japan"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fscj.4690171102","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/scj.4690171102","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,21]],"date-time":"2023-10-21T13:36:21Z","timestamp":1697895381000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/scj.4690171102"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1986,1]]},"references-count":15,"journal-issue":{"issue":"11","published-print":{"date-parts":[[1986,1]]}},"alternative-id":["10.1002\/scj.4690171102"],"URL":"https:\/\/doi.org\/10.1002\/scj.4690171102","archive":["Portico"],"relation":{},"ISSN":["0882-1666","1520-684X"],"issn-type":[{"value":"0882-1666","type":"print"},{"value":"1520-684X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1986,1]]}}}