A model of actors and grey failures

TL;DR

This paper introduces a novel actor-based system model that incorporates grey failures, capturing transient and subtle faults, and provides a behavioral equivalence framework to analyze system reliability and recovery.

Contribution

It extends existing models by including grey failures and offers a bisimulation-based method to verify system reliability properties.

Findings

Model captures fail-stop and grey failures including transient faults.

Behavioral equivalence based on weak barbed bisimulation for reliability analysis.

Reduces reliability verification to bisimulation checking.

Abstract

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.