Distributed systems can be subject to various kinds of partial failures, therefore building fault-tolerance or failure mitigation mechanisms for distributed systems remains an important domain of research. In this paper, we present a calculus to formally model distributed systems subject to crash failures with recovery. The recovery model considered in the paper is weak, in the sense that it makes no assumption on the exact state in which a failed node resumes its execution, only its identity has to be distinguishable from past incarnations of itself. Our calculus is inspired in part by the Erlang programming language and in part by the distributed $\pi$-calculus with nodes and link failures (D$\pi$F) introduced by Francalanza and Hennessy. In order to reason about distributed systems with failures and recovery we develop a behavioral theory for our calculus, in the form of a contextual equivalence, and of a fully abstract coinductive characterization of this equivalence by means of a labelled transition system semantics and its associated weak bisimilarity. This result is valuable for it provides a compositional proof technique for proving or disproving contextual equivalence between systems.

翻译：分布式系统可能遭受各种类型的部分故障，因此为分布式系统构建容错或故障缓解机制仍然是重要的研究领域。本文提出了一种演算方法，用于形式化建模受崩溃故障及恢复影响的分布式系统。本文考虑的恢复模型是弱恢复模型，这意味着它不对故障节点恢复执行时的确切状态做出任何假设，仅要求其身份能够与自身的过往实例相区分。我们的演算部分受Erlang编程语言启发，部分借鉴了Francalanza和Hennessy提出的具有节点与链路故障的分布式π演算（DπF）。为了对具有故障和恢复的分布式系统进行推理，我们为该演算建立了行为理论，具体表现为上下文等价关系，以及通过带标签的转移系统语义及其关联的弱互模拟关系对此等价关系给出的完全抽象的共归纳刻画。这一结果具有重要价值，因为它为证明或证否系统间的上下文等价关系提供了组合式证明技术。