On proving communication closedness of distributed layers
Lecture notes in computer sciencePublished 1 January 1986
Rob Gerth, Liuba Shrira
Citations16
SJR quartileQ2
SJR score0.35
SNIP0.55
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
A proof rule proving closedness of a distributed layer is developed as an extension of the Apt, Francez and de Roever proof system for CSP and is proved to be sound and relatively complete.
Abstract
The notion of communication closed layer has been introduced as a way to define structured composition of distributed systems. An interesting question is how to verify the closedness of a layer. We formulate a proof rule proving closedness of a distributed layer. The rule is developed as an extension of the Apt, Francez and de Roever proof system for CSP. The extension is proved to be sound and relatively complete.
Keywords
Computer Science
ACM Transactions on Programming Languages and SystemsA Proof System for Communicating Sequential Processes
324 Citations1980Krzysztof R. Apt, Nissim Francez +1 more
An axiomatic proof system is presented for proving partial correctness and absence of deadlock of communicating sequential processes, the key (meta) rule introduces cooperation between proofs, and CSP's new convention for distributed termination of loops is dealt with.
Science of Computer ProgrammingDecomposition of distributed programs into communication-closed layers
206 Citations1982Tzilla Elrad, Nissim Francez
The safe decomposition of a distributed program into communication closed layers is suggested as a superstructure of its decomposition into a collection of communicating processes.
Lecture notes in computer scienceCompositionality and concurrent networks: Soundness and completeness of a proofsystem
77 Citations1985Job Zwiers, Willem P. de Roever +1 more
A compositional proofsystem is presented for a language that includes parallel executing networks and recursive creation of subnetworks and is shown to be arithmetically complete.
Control Flow and Data Flow: Concepts of Distributed Programming
67 Citations1986Manfred Broy
This book discusses Operational Models of Distributed Systems, Partial Orderings of Events, and Event Structures, and Design and Verification of Distribution Systems.
Journal of the ACMFormal Justification of a Proof System for Communicating Sequential Processes
61 Citations1983Krzysztof R. Apt
Soundness and relative completeness of this proof system dealing with partial correctness of communicating sequential processes are proved and it is indicated in what way the semantics and the proof system can be extended to deal with the total correctness of the programs.
Theoretical Computer ScienceA linear-history semantics for languages for distributed programming
55 Citations1984Nissim Francez, Daniel Lehmann +1 more
A denotational semantics is given for a language for distributed programming based on communication (CSP) that uses both linear sequences of communications to record computations and special states, called ‘expectation sets’, characterizing potential deadlocks.
Distributed k-selection
38 Citations1983Liuba Shrira, Nissim Francez +1 more
A methodology for transforming sequential recursive algorithms to distributive ones is suggested and it is suggested that the program segments between recursive calls have a distributive implementation.
Science of Computer ProgrammingA proof system for concurrent ADA programs
35 Citations1984Rob Gerth, Willem P. de Roever
A Hoare-style proof system for proving partial correctness properties which is sound and relatively complete is developed, then extended to deal with safety, deadlock, termination and failure.
Fundamenta InformaticaeProving Monitors Revisited: A First Step Towards Verifying Object Oriented Systems1
14 Citations1986Rob Gerth, Willem P. de Roever
An axiomatic characterization of monitors, based on assumption-commitment style reasoning, is given that is sound and (relatively) complete that is a first step towards the formal verification of object oriented systems.
Science of Computer ProgrammingAutomatic construction of CSP programs from sequential non-deterministic programs
6 Citations1985Abha Moitra
The two versions of the program are shown to be strongly equivalent, in the sense that they exhibit the properties of reaching the same final states and of either aborting, terminating, or running forever.