一句话：提出带灰色故障的 actor 系统模型与弱 barbed 互模拟等价，将可靠性验证归约为互模拟检查。
现有并发进程分析模型多假设 fail-stop 故障，即进程要么工作要么永久停止，且状态已知；但实际系统常出现灰色故障：潜在、可能瞬态，并以隐蔽方式影响系统，进而引发崩溃、可用性受限或过载等严重问题。论文提出基于两层的 actor 系统模型：一层是带离散时间的异步进程演算 actor 模型，另一层是可向系统注入故障的故障模式模型，既覆盖 fail-stop 的节点与链路故障，也刻画部分、瞬态等灰色故障。作者定义基于弱 barbed bisimulation 的行为等价，以系统从故障恢复的能力比较系统，并据此给出可靠系统的若干理想性质，从而将系统可靠性性质的检查归约为互模拟检查。
Existing models for the analysis of concurrent processes tend to focus on fail-stop failures, where processes are either working or permanently stopped, and their state (working/stopped) is known. In fact, systems are often affected by grey failures: failures that are latent, possibly transient, and may affect the system in subtle ways that later lead to major issues (such as crashes, limited availability, overload). We introduce a model of actor-based systems with grey failures, based on two interlinked layers: an actor model, given as an asynchronous process calculus with discrete time, and a failure model that represents failure patterns to inject in the system. Our failure model captures not only fail-stop node and link failures, but also grey failures (e.g., partial, transient). We give a behavioural equivalence relation based on weak barbed bisimulation to compare systems on the basis of their ability to recover from failures, and on this basis we define some desirable properties of reliable systems. By doing so, we reduce the problem of checking reliability properties of systems to the problem of checking bisimulation.
@article{paperbot2181,
title = {A model of actors and grey failures},
author = {Laura Bocchi and Julien Lange and Simon Thompson and A. Laura Voinea},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 4},
year = {2023},
doi = {10.46298/lmcs-19(4:13)2023}
}