An STREL-based Formulation of Spatial Resilience in Cyber-Physical Systems

TL;DR

This paper introduces a formal framework based on STREL for analyzing spatial resiliency in Cyber-Physical Systems, providing a way to specify, quantify, and evaluate recoverability and persistency over spatial routes.

Contribution

It develops a novel formal model and semantics for spatial resiliency using SREL, including algorithms for evaluating resilience metrics and case studies demonstrating practical application.

Findings

Defined a Spatial Resilience Specification (SpaRS) framework.

Proved soundness and completeness of the SpaRV semantics.

Demonstrated practical utility through case studies.

Abstract

Resiliency is the ability of a system to quickly recover from a violation (recoverability) and avoid future violations for as long as possible (durability). In the spatial setting, recoverability and durability (now known as persistency) are measured in units of distance. Like its temporal counterpart, spatial resiliency is of fundamental importance for Cyber-Physical Systems (CPS) and yet, to date, there is no widely agreed-upon formal treatment of spatial resiliency. We present a formal framework for reasoning about spatial resiliency in CPS. Our framework is based on the spatial fragment of STREL, which we refer to as SREL. In this framework, spatial resiliency is given a syntactic characterization in the form of a Spatial Resiliency Specification (SpaRS). An atomic predicate of SpaRS is called an S-atom. Given an arbitrary SREL formula $\varphi$, distance bounds $d_1, d_2$, the S-atom of $\varphi$, $S_{d_1, d_2} (\varphi)$, is the SREL formula $\neg\varphi R_{[0,d_1]} (\varphi R_{[d_2, +\infty)}\varphi)$, specifying that recovery from a violation of $\varphi$ occurs within distance $d_1$ (recoverability), and subsequently that $\varphi$ be maintained along a route for a distance greater than $d_2$ (persistency). S-atoms can be combined using spatial STREL operators, allowing one to express composite resiliency specifications. We define a quantitative semantics for SpaRS in the form of a Spatial Resilience Value (SpaRV) function $\sigma$ and prove its soundness and completeness w.r.t. SREL's Boolean semantics. The $\sigma$-value for $S_{d_1,d_2}(\varphi)$ is a set of non-dominated (rec, per) pairs, quantifying recoverability and persistency, given that some routes may offer better recoverability while others better persistency. In addition, we design algorithms to evaluate SpaRV for SpaRS formulas. Finally, two case studies demonstrate the practical utility of our approach.