Algebraic specification and proof of a distributed recovery algorithm

DOI10.1007/BF01786251MaRDI QIDQ1090102zbMATH OpenFDO

Authors Jifeng He, Tony Hoare

Publication date 1987

Published in Distributed Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BF01786251

zbMATH Keywords

Communicating Sequential Processesdeterministic processfixed pointproofs of correctness

Mathematics Subject Classification ID

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

Review text

An algebraic specification is given of an algorithm for recovery from catastrophe by a deterministic process. A second version of the algorithm also includes check-points. The algorithms are formulated in the notations of Communicating Sequential Processes [\textit{C. A. R. Hoare}, Prentice-Hall (Englewood Cliffs 1985)] and the proofs of correctness are conducted wholly by application of algebraic laws (together with the unique fixed point theorem).

Recommendations

• scientific article; zbMATH DE number 4018375
• scientific article; zbMATH DE number 3872655
• scientific article; zbMATH DE number 3936493
• Algebraic specification of reactive systems
• Much ado about nothing?

Cites work

• A Transformation System for Developing Recursive Programs
• Can programming be liberated from the von Neumann style?
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• Time, clocks, and the ordering of events in a distributed system

Cited in

(8)

• Design and verification of fault tolerant systems with CSP
• Transformation of programs for fault-tolerance
• A compositional framework for fault tolerance by specification transformation
• A trace-based compositional proof theory for fault tolerant distributed systems
• Modular specification of process algebras
• Lax naturality through enrichment
• A computer checked algebraic verification of a distributed summation algorithm
• Second-level algorithms, superrecursivity, and recovery problem in distributed systems

This page was built for publication: Algebraic specification and proof of a distributed recovery algorithm

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