Verification system for partial correctness of communicating sequential processes

Masaki Murakami, Yasuyoshi Inagaki

Research output: Contribution to journalArticle

1 Citation (Scopus)

Abstract

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‐output 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.

Original languageEnglish
Pages (from-to)11-20
Number of pages10
JournalSystems and Computers in Japan
Volume17
Issue number11
DOIs
Publication statusPublished - 1986
Externally publishedYes

ASJC Scopus subject areas

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

Fingerprint Dive into the research topics of 'Verification system for partial correctness of communicating sequential processes'. Together they form a unique fingerprint.

Cite this