Proof rules for fault tolerant distributed programs

DOI10.1016/0167-6423(87)90003-7MaRDI QIDQ1085970zbMATH OpenOpenAlexFDO

Authors Mathai Joseph, Abha Moitra, N. Soundararajan

Publication date 1987

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://hdl.handle.net/1813/6482

zbMATH Keywords

distributed systemfault tolerant propertieshardware failuresHoare's CSPprocessing nodesproof system

Mathematics Subject Classification ID

Theory of operating systems (68N25) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

Proving the properties of a program which must execute on a distributed system whose nodes may fail is a complex task. Such proofs must take into account the effects of hardware failures at all possible points in the execution of individual processes. The difficulty in accomplishing this is compounded by the need to cater also for the simultaneous failure of two or more processing nodes. In this paper, we consider programs written in a version of Hoare's CSP and define a set of axioms and inference rules by which proofs can be constructed in three steps: proving the properties of each process when its communicants are prone to failure, establishing the effects of failure of each process, and combining these two steps to determine the fault tolerant properties of the whole program. The proof system is thus compositional, in the sense that proofs can be constructed in a modular way.

Recommendations

• A trace-based compositional proof theory for fault tolerant distributed systems
• scientific article; zbMATH DE number 3903944
• scientific article; zbMATH DE number 3846851
• A compositional proof system for distributed programs
• P-A logic - a compositional proof system for distributed programs

Cited in

(9)

• Transformation of programs for fault-tolerance
• A trace-based compositional proof theory for fault tolerant distributed systems
• Redundancy in distributed proofs
• A theory for observational fault tolerance
• scientific article; zbMATH DE number 3846851 (Why is no real title available?)
• Faulty Logic: Reasoning about Fault Tolerant Programs
• scientific article; zbMATH DE number 3900140 (Why is no real title available?)
• A Fault Tolerance Bisimulation Proof for Consensus (Extended Abstract)
• P-A logic - a compositional proof system for distributed programs

This page was built for publication: Proof rules for fault tolerant distributed programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1085970)