# Stark: A Software Tool for the Analysis of Robustness in the unKnown Environment

Valentina Castiglioni, Michele Loreti, Simone Tini

► To cite this version:

Valentina Castiglioni, Michele Loreti, Simone Tini. Stark: A Software Tool for the Analysis of Robustness in the unKnown Environment. 25th International Conference on Coordination Languages and Models (COORDINATION), Jun 2023, Lisbon, Portugal. pp.115-132, 10.1007/978-3-031-35361-1_6. hal-04673811

HAL Id: hal-04673811

https://inria.hal.science/hal-04673811v1

Submitted on 20 Aug 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
<figure><img src="image_2.png" /></figure>

ifip

International Federation for Information Processing

This document is the original author manuscript of a paper submitted to an IFIP
conference proceedings or other IFIP publication by Springer Nature. As such, there
may be some differences in the official published version of the paper. Such
differences, if any, are usually due to reformatting during preparation for publication or
minor corrections made by the author(s) during final proofreading of the publication
manuscript.
# STARK: A Software Tool for the Analysis of Robustness in the unKnown environment

Valentina Castiglioni<fnref n="1" /> Ⓒ, Michele Loreti<fnref n="2" /> Ⓒ, and Simone Tini<fnref n="3" /> Ⓒ

**Abstract.** Cyber-Physical Systems (CPSs) are characterised by the interaction of various agents operating under highly changing and, sometimes, unpredictable environmental conditions. It is therefore fundamental to verify whether these systems are *robust against perturbations*, i.e., whether systems are able to function correctly even in perturbed circumstances. In this paper we present the *Software Tool for the Analysis of Robustness in the unKnown environment* (STARK), our Java tool for the specification, analysis and testing of robustness properties of CPSs. STARK includes: (i) a specification language for systems behaviour, perturbations, distances on systems behaviours, and properties of those distances; (ii) a module for the simulation of system behaviours and their perturbed versions; (iii) a module for the evaluation of distances between behaviours; (iv) a statistical model checker for formulae in the *Robustness Temporal Logic (RobTL)*, a temporal logic for the specification and verification of properties on the evolution of *distances* between the behaviours of CPSs, and thus also of robustness properties.

## 1 Introduction

Cyber-Physical Systems (CPSs) are characterised by the interaction of various agents operating under highly changing and, sometimes, unpredictable environmental conditions. For instance, the dynamic physical environmental processes can only be approximated in order to become computationally tractable; some agents may appear, disappear, or become temporarily unavailable, thus causing faults or conflicts; sensors may introduce measurement errors; etc. This means that the behaviour of the agents in a CPS is subject to uncertainty and perturbations. On top of that, there is a class of security threats which is unique to CPSs, namely cyber-physical attacks: for instance, an attacker can induce a series of perturbations in the sensed data in order to entail unexpected, hazardous, behaviour of the system.

It is therefore fundamental to verify whether a CPS is *robust against perturbations*, i.e., whether the system is able to function correctly even in the presence of perturbations. Although there is lack of agreement on the “correct” mathematical formalisation of robustness (see, e.g., [9, 21, 23, 24]), this notion is usually presented as a *measure* of the capability of a system to tolerate perturbations in the environmental conditions and still fulfil its tasks. In other words, robustness can be specified, in general, as a temporal property of distances between the nominal and the perturbed behaviours of a system. To this purpose, we have recently proposed the *Robustness Temporal Logic (RobTL)* [4]

<footnote n="1">¹ Reykjavik University, Reykjavik, Iceland</footnote>

<footnote n="2">² University of Camerino, Camerino, Italy</footnote>

<footnote n="3">³ University of Insubria, Como, Italy</footnote>
to capture robustness properties: RobTL is the first temporal logic for the specification and analysis of distances between the behaviours of CPSs over a finite time horizon.

In this paper we pursue our quest for a formal framework allowing us to specify and analyse distances between behaviours of systems operating in the presence of uncertainties, by presenting the *Software Tool for the Analysis of Robustness in the unKnown environment* (STARK), available at https://github.com/quasylab/jspear^4. STARK is a Java tool for the specification, analysis and testing of robustness properties of CPSs that is based on the *evolution sequence* model from [3] for the representation of systems behaviour, and on RobTL for the specification of distances, perturbations, and properties. Briefly, evolution sequences are countable sequences of probability measures over a set of application-relevant data, each representing the interaction of the agents with the environment at a given time step. Then, atomic propositions in RobTL are defined by means of two simple languages: one to specify the effect of *perturbations* over an evolution sequence, and one to specify *distance expressions* between an evolution sequence and its perturbed version.

Specifically, STARK consists of a front-end and a Java library, and includes:

- A specification language for the system (agents, environment, and their interaction), for perturbations, for distance expressions, and for RobTL formulae;

- A module for the simulation of systems behaviours and their perturbed versions;

- A module for the evaluation of distances between behaviours;

- A statistical model checker for RobTL formulae.

We remark that since the simulation of system behaviours and the evaluation of distances are based on statistical inference, the evaluation of RobTL formulae is based on a three-valued semantics that takes possible statistical errors into account.

To showcase the various features of the tool, we apply it to a case-study in the analysis of CPSs proposed in [18]: we consider two unmanned ground vehicles that are moving along a straight path, in line, and have to autonomously set their acceleration in order to avoid collision with a static obstacle. Moreover, the second vehicle needs also to avoid collisions with the first one. We model both cyber-physical attacks and equipment malfunctioning in terms of perturbations in sensed data, and we study the robustness of the vehicles against the attacks and malfunctioning.

## 2 The Model

We consider systems consisting of a set of agents and an environment, whose interaction produces changes on a shared data space $D$, containing the values assumed by variables, representing: (i) physical quantities, (ii) sensors, (iii) actuators, and (iv) internal variables of the agents. We call *system configuration* the triple consisting of the set of internal states of the agents, the set of functions constituting the environment, and the current state of the data space, called *data state* and represented by a mapping $d$ from variables to values. At each step, the agents and the environment induce some changes on the data state providing thus a new data state at the next step. Those modifications are also subject to the presence of uncertainties, meaning that it is not always possible

<footnote>^4 The tool has been also published on *Software Heritage* with ID `swh:1:dir:98532d8c770f9d115c692e932869c446417d8b34`</footnote>
<figure><img src="image_3.png" /><figcaption>Fig. 1: The two agents and their variables: in black we report the main physical (real) data, in blue the sensed data by V1, and in red those by V2. See Table 1 for the complete list of variables.</figcaption></figure>

to determine exactly the values assumed by data at the next step. Hence, following [3], we model the changes induced at each step as a probability measure on the attainable data states. The behaviour of the system is then entirely expressed by its evolution sequence, i.e., the sequence of probability measures over the data states obtained at each step. In other words, the evolution sequence is the discrete-time version of the cylinder of all possible trajectories of the system. In this paper we do not focus on how evolution sequences are generated: we simply assume a Markov kernel governing the evolution of the system, and the evolution sequence is the Markov process generated by it. We refer the interested reader to [3] for the details on the specification of the agents and the environment, and on the semantic mapping allowing for deriving the Markov kernel at hand.

**Definition 1 (Evolution sequence, [3]).** Given a data space $\mathcal{D}$, let $\mathcal{B}_\mathcal{D}$ denote the Borel $\sigma$-algebra over $\mathcal{D}$, and let $\Pi(\mathcal{D}, \mathcal{B}_\mathcal{D})$ be the set of probability measures (henceforth simply called distributions) over the space $(\mathcal{D}, \mathcal{B}_\mathcal{D})$.

Assume a Markov kernel step: $\mathcal{D} \to \Pi(\mathcal{D}, \mathcal{B}_\mathcal{D})$ generating the behaviour of a system $s$ having $\mu$ as initial distribution. Then, the evolution sequence of $s$ is a countable sequence $S_\mu = S_\mu^0, S_\mu^1, \dots$ of distributions in $\Pi(\mathcal{D}, \mathcal{B}_\mathcal{D})$ such that, for all $\mathcal{D} \in \mathcal{B}_\mathcal{D}$:

$$S_{\mu}^{0}(\mathcal{D}) = \mu(\mathcal{D}) \qquad S_{\mu}^{i+1}(\mathcal{D}) = \int_{\mathcal{D}} \text{step}(\mathbf{d})(\mathcal{D}) \circ S_{\mu}^{i}(\mathbf{d}).$$

## 2.1 Case Study: Unmanned Ground Vehicles

We present the case study that will allow us to showcase the features of our tool. We consider two unmanned ground vehicles, agents V1 and V2, that have to autonomously set their acceleration in order to avoid collisions with a static obstacle and with each other. This example was originally proposed, with a single vehicle, in [18]. We remark that our aim is not to specify a complex real-world scenario, but rather to illustrate an application of the tool. Hence, we model the system in a simplified setting: we consider the agents and the obstacle as one-dimensional objects (as done in, e.g., [6, 27]), we assume that the two agents are identical, that they can move only along one direction, proceeding in line, and we consider simple versions of their control units.

Figure 1 illustrates our setting for the system: $Vx$ is at $p\_distance\_Vx$ m from the obstacle and moves towards it at a speed of $p\_speed\_Vx$ m/s. Then, the distance between
<table><caption>Table 1: The variables, $x \in \{1, 2\}$.</caption><thead><tr><th>Name</th><th>Domain</th><th>Role</th></tr></thead><tbody><tr><td>p_speed_Vx</td><td>[0, MAX_SPEED]</td><td>physical speed of Vx (m/s)</td></tr><tr><td>s_speed_Vx</td><td>[0, MAX_SPEED]</td><td>sensor detecting the value of p_speed_Vx</td></tr><tr><td>p_distance_Vx</td><td>[0, INIT_DISTANCE_Vx]</td><td>distance of Vx from the obstacle (m)</td></tr><tr><td>s_distance_Vx</td><td>[0, INIT_DISTANCE_Vx]</td><td>sensor detecting the value of p_distance_Vx</td></tr><tr><td>accel_Vx</td><td>{A, N, -B}</td><td>actuator for acceleration (m/s²), with A, B > 0, N = 0</td></tr><tr><td>timer_Vx</td><td>[0, TIMER]</td><td>countdown for checks by the controller of Vx</td></tr><tr><td>braking_dist_Vx</td><td>[0, INIT_DISTANCE_Vx]</td><td>space required by Vx to stop if accel_Vx = -B</td></tr><tr><td>required_dist_Vx</td><td>[0, INIT_DISTANCE_Vx]</td><td>braking_dist_Vx plus SAFETY_DISTANCE</td></tr><tr><td>safety-gap_Vx</td><td>[0, INIT_DISTANCE_Vx]</td><td>p_distance_Vx - required_dist_Vx</td></tr><tr><td>brake_light_Vx</td><td>{0, 1}</td><td>actuator for brake lights of Vx (1 = ON)</td></tr><tr><td>p_distance_V1_V2</td><td>[0, INIT_DISTANCE_V1_V2]</td><td>distance of V2 from V1 (m)</td></tr><tr><td>s_distance_V1_V2</td><td>[0, INIT_DISTANCE_V1_V2]</td><td>sensor detecting the value of p_distance_V1_V2</td></tr><tr><td>safety-gap_V1_V2</td><td>[0, INIT_DISTANCE_V1_V2]</td><td>p_distance_V1_V2 - required_dist_V2</td></tr><tr><td>crashed_Vx</td><td>{0, 1}</td><td>gets 1 if a collision occurred</td></tr><tr><td>warning_Vx</td><td>{0, 1}</td><td>message from IDS_Vx (1 = DANGER)</td></tr></tbody></table>

the two vehicles is p_distance_V1_V2 m. These values are detected by the controllers of V1 and V2 through sensors s_distance_Vx, s_speed_Vx, and s_distance_V1_V2, respectively. For simplicity, we assume that the values detected by sensors coincide with the physical ones, i.e., that there are no measurements errors. We will introduce noise and tampering on sensors later on, by means of perturbations. The vehicles can either accelerate or brake. In the former case, a vehicle has a positive acceleration, A m/s². In the latter case, the vehicle has a negative acceleration, whose absolute value corresponds to B m/s². When Vx brakes, the brake lights are switched on, as expressed by actuator brake-light_Vx. The controller of Vx, for $x \in \{1, 2\}$, checks regularly whether Vx can safely accelerate or if it has to brake, and sets the acceleration actuator accel_Vx accordingly. The decision is taken by the controller on the basis of both the speed of Vx and its distance from the obstacle, or (for V2) from the preceding vehicle. V2 brakes also when the lights of V1 are on. The decision between accelerating or braking is taken by the controller every TIMER seconds: variable timer_Vx is initially set to TIMER and the controller is woken up whenever it reaches zero. The speed can never be negative, and when the speed becomes zero then the actuator accel_Vx is set to N = 0.

The variables are listed in Table 1. Besides the variables associated to physical quantities, actuators and sensors described above, we use: (i) braking_dist_Vx for the space required to stop Vx if it starts to brake immediately; (ii) required_dist_Vx for braking_dist_Vx incremented by constant SAFETY_DISTANCE; (iii) safety-gap_Vx for the difference between p_distance_Vx and required_dist_Vx, and safety-gap_V1_V2 for that between p_distance_V1_V2 and required_dist_V2: if a safety gap is negative, the vehicles are at risk of a collision; (iv) crashed_Vx to signal if Vx collided either against the obstacle or the other vehicle.

Each controller is paired with an intrusion detection system IDS_Vx, whose task is to detect odd or hazardous behaviours. In case of anomalies, IDS_Vx uses variable warning_Vx to raise a warning message and induce the controller to react. Specifically, IDS_Vx checks whether the physical distances are large enough to guarantee a
safe behaviour, expressed as p_distance_V1 > 2 · TIMER · SAFETY_DISTANCES and p_distance_V1_V2 > 2 · TIMER · SAFETY_DISTANCES; if this is not the case and Vx has a positive acceleration, the warning is raised, and Vx is required to decelerate.

## 3 The Robustness Temporal Logic

The Robustness Temporal Logic (RobTL) has been introduced in [4] as the first logic allowing one to express temporal properties of distances over systems behaviours. It is the core of our tool for the specification and analysis of robustness properties of CPSs against uncertainties and perturbations. This is made possible by using atomic propositions of the form Δ(exp, p) ⋈ η to evaluate the distance specified by an expression exp at a given time step between a given evolution sequence and its perturbed version, obtained by some perturbation p, and to compare it with the threshold η. Then, we combine atomic propositions with classic Boolean and temporal operators, in order to extend these evaluations to the entire evolution sequences.

Hence, there are three main components constituting RobTL formulae: 1. A language Exp to specify distance expressions; 2. A language P to specify perturbations; 3. Classic Boolean and temporal operators to specify requirements on the evolution of distances in time. In this section we give only a bird's-eye view on these components. We refer the interested reader to [4] for a detailed presentation of RobTL.

**Distance Expressions** We use expressions in Exp to define distances over evolution sequences. The idea is to introduce a distance over distributions on data states measuring their differences with respect to a given target, and then use the operators of the logic to extend it to the evolution sequences, while possibly taking into account different objectives and perturbations over time. Following [3], to capture a particular task, we use a penalty function ρ: D → [0, 1], i.e., a function that assigns to each data state d a penalty in [0, 1] expressing how far the values of the parameters related to the considered task in d are from their desired ones. Then we use ρ to obtain a distance on data states, i.e., the 1-bounded hemimetric mρ defined for all d₁, d₂ ∈ D by:

$$m_{\rho}(\mathbf{d}_1, \mathbf{d}_2) = \max\{\rho(\mathbf{d}_2) - \rho(\mathbf{d}_1), 0\}.$$

Note that mρ(d₁, d₂) expresses how much d₂ is worse than d₁ according to ρ. Then, we need to lift the hemimetric mρ to a hemimetric over Π(D, B_D). To this end, we make use of the Wasserstein lifting [25]: for any two distributions μ, ν on (D, B_D), the Wasserstein lifting of mρ to a distance between μ and ν is defined by

$$\mathbf{W}(m_{\rho})(\mu, \nu) = \inf_{\mathfrak{w} \in \mathfrak{W}(\mu, \nu)} \int_{D \times D} m_{\rho}(\mathbf{d}, \mathbf{d}') \, d\mathfrak{w}(\mathbf{d}, \mathbf{d}')$$

where W(μ, ν) is the set of the couplings of μ and ν, namely the set of joint distributions w over the product space (D × D, B(D × D)) having μ and ν as left and right marginal, respectively, i.e., w(D × D) = μ(D) and w(D × D) = ν(D), for all D ∈ B(D).
**Definition 2 (Distance expressions).** Expressions in Exp are defined as follows:

$$ \exp ::= \langle \rho \mid \rangle^{\rho} \mid \mathbf{F}^{I} \exp \mid \mathbf{G}^{I} \exp \mid \exp \mathbf{U}^{I} \exp \mid \\ \min(\exp, \exp) \mid \max(\exp, \exp) \mid \sum_{k \in K} w_k \cdot \exp_k \mid \sigma(\exp, \bowtie \zeta) $$

where $\rho$ ranges over penalty functions, $I$ is an interval, $K$ is a finite set of indexes, $w_k \in (0, 1]$ for each $k \in K$, $\sum_{k \in K} w_k = 1$, and $\zeta \in [0, 1]$.

Distance expressions are evaluated over a pair of evolution sequences and a time step: given two evolution sequences $S_1, S_2$ and a time step $\tau$, the evaluation of expressions in the triple $S_1, S_2, \tau$ is given by function $[\cdot]_{S_1, S_2}^{\tau}$: $\text{Exp} \to [0, 1]$ which is defined inductively over expressions. It bases on two atomic expressions, $<\rho>$ and $>\rho$, where $\rho$ is a penalty function, as follows:

$$ [[<\rho]]_{S_1, S_2}^{\tau} = \mathbf{W}(m_{\rho})(S_1^{\tau}, S_2^{\tau}) \qquad [[>\rho]]_{S_1, S_2}^{\tau} = \mathbf{W}(m_{\rho})(S_2^{\tau}, S_1^{\tau}). $$

Then we provide three temporal expression operators, namely $\mathbf{F}^I$, $\mathbf{G}^I$ and $\mathbf{U}^I$, allowing for the evaluation of minimal and maximal distances over time: their semantics follows from that of the corresponding (bounded) temporal operators (resp., eventually, always, and until) by associating existential quantifications with minima, and universal quantifications with maxima. The $\min$, $\max$ and convex combination $\sum_K w_k$ operators are as expected. The comparison operator $\sigma(\text{exp}, \bowtie \zeta)$ returns a value in $\{0, 1\}$ used to establish whether the evaluation of $\text{exp}$ is in relation $\bowtie$ with the threshold $\zeta$. Summarising, by means of expressions we can measure the differences between evolution sequences with respect to various tasks (penalty functions) and temporal constraints.

**Perturbations** A perturbation is the effect of unpredictable events, that can be repeated or different in time, on the current state of the system. In [4], a perturbation is therefore modelled as a time-dependent function that maps a data state into a distribution over data states. Specifically, a perturbation $p$ is a list of mappings in which the $i$-th element describes the effects of $p$ at time $i$, and that is specified in the following language:

**Definition 3 (Perturbations).** Perturbations in P are defined as follows:

$$ p ::= \text{nil} \mid \text{f@}\tau \mid p_1; p_2 \mid p^n $$

where $p$ ranges over $P$, $n$ and $\tau$ are finite natural numbers, and:

- $\text{nil}$ is the perturbation with no effects, i.e., at each time step it behaves like the identity function $\text{id}: \mathcal{D} \to \Pi(\mathcal{D}, \mathcal{B}_{\mathcal{D}})$ such that $\text{id}(\mathbf{d}) = \delta_{\mathbf{d}}$ for all $\mathbf{d} \in \mathcal{D}$, with $\delta_{\mathbf{d}}$ the Dirac distribution defined by $\delta_{\mathbf{d}}(\mathcal{D}) = 1$ if $\mathbf{d} \in \mathcal{D}$ and $\delta_{\mathbf{d}}(\mathcal{D}) = 0$ otherwise;

- $\text{f@}\tau$ is an atomic perturbation, i.e., a function $\text{f}: \mathcal{D} \to \Pi(\mathcal{D}, \mathcal{B}_{\mathcal{D}})$ such that the mapping $\mathbf{d} \mapsto \text{f}(\mathbf{d})(\mathcal{D})$ is $\mathcal{B}_{\mathcal{D}}$-measurable for all $\mathcal{D} \in \mathcal{B}_{\mathcal{D}}$, and that is applied after $\tau$ time steps from the current instant;

- $p_1; p_2$ is a sequential perturbation, i.e., perturbation $p_2$ is applied at the time step subsequent to the (final) application of $p_1$;
- p^n is an iterated perturbation, i.e., perturbation p is applied for a total of n times.

The semantics of perturbations is then defined by means of two auxiliary functions: effect(p), that describes the effect of p at the current step, and next(p), that identifies the perturbation that will be applied at the next step. These two functions are defined inductively over the structure of p. Due to space limitations, we omit their formal definition, and refer the interested reader to [4]. We make use of effect and next to define the mapping $\langle\cdot\rangle: P \to (D \times N \to \Pi(D, B_D))$ such that, for all $d \in D$ and $i \in N$:

$$ \langle\langle p \rangle\rangle(d, i) = \text{effect}(\text{next}^i(p))(d), $$

where $\text{next}^0(p) = p$ and $\text{next}^i(p) = \text{next}(\text{next}^{i-1}(p))$, for all $i > 0$.

Now we can define the perturbation of an evolution sequence.

**Definition 4 (Perturbation of an evolution sequence).** Given an evolution sequence $S_\mu$, with $\mu$ as initial distribution, and a perturbation p, we define the perturbation of $S_\mu$ via p as the evolution sequence $S_\mu^P$ obtained as follows:

$$ S_{\mu}^{P,0}(D) = \int_{D} \langle\langle p \rangle\rangle(d, 0)(D) \mathfrak{d} \mu(d) $$

$$ S_{\mu}^{P,i+1}(D) = \int_{D} \left( \int_{D} \langle\langle p \rangle\rangle(d', i+1)(D) \mathfrak{d} \text{step}(d)(d') \right) \mathfrak{d} S_{\mu}^{P,i}(d), $$

where function step is the Markov kernel that generates $S_\mu$.

**Remark 1.** Functions effect and next are such that, for each $i \in N$, $\langle\langle p \rangle\rangle(d, i)$ is either the Dirac distribution over $d$, or the distribution $f(d)$ induced by an atomic perturbation with function $f$. In both cases, the mapping $d \mapsto \langle\langle p \rangle\rangle(d, i)(D)$ is guaranteed to be $B_D$-measurable for all $D \in B_D$. Hence, the integrals in Definition 4 are well defined (see also [4, Proposition 4.7]).

**RobTL Formulae** We use formulae in RobTL for the specification and analysis of distances between nominal and perturbed evolution sequences over a finite time horizon, henceforth denoted by $\mathfrak{h}$. The idea is that by combining atomic propositions with temporal operators, we can apply (possibly) different distance expressions and perturbations at different time steps, thus allowing for the analysis of systems behaviour in complex scenarios.

**Definition 5 (RobTL).** RobTL consists in the set of formulae L defined by:

$$ \varphi ::= \top \mid \Delta(\exp, p) \bowtie \eta \mid \neg \varphi \mid \varphi \wedge \varphi \mid \varphi \mathcal{U}^I \varphi $$

where $\varphi$ ranges over L, $\exp$ ranges over expressions in Exp, $p$ ranges over perturbations in P, $\bowtie \in \{<, \leq, \geq, >\}$, $\eta \in [0, 1]$, and $I \subseteq [0, \mathfrak{h}]$ is a bounded time interval.

Formulae are evaluated in an evolution sequence and a time instant. Notice that, due to the presence of uncertainties and probability, the procedures that we use to 1. simulate the evolution sequences and the effects of perturbations, and 2. evaluate distance
expressions, are based on statistical inference. Hence, the presence of statistical errors has to be taken into account also when checking the satisfaction of RobTL formulae. Consequently, our model checker will assign a three-valued semantics to formulae by adding the truth value unknown (U) to the classic true (T) and false (F). Intuitively, unknown is generated by the comparison between the distance and the chosen threshold in atomic propositions: if the threshold η does not lie in the confidence interval of the evaluation of the distance, then the formula will evaluate to T or F according to whether the relation ⋇ η holds or not. Conversely, if η belongs to the confidence interval, then the atomic proposition evaluates to U, since the validity of the relation ⋇ η may depend on the particular samples obtained in the simulation. Starting from atomic propositions, the three-valued semantics is extended to the Boolean and temporal operators in the standard way [13, 26]. We assign a three-valued semantics to RobTL formulae via the satisfaction function Ω_S: L × [0, h] → {T, U, F}, defined inductively on the structure of RobTL formulae. Specifically, on atomic propositions Ω_S is defined as follows:

$$ \Omega_S(\Delta(\mathbf{exp}, p) ⋇ \eta, \tau) = \begin{cases} U & \text{if } \eta \in \mathrm{CI}_{\mathrm{exp}} \\ T & \text{if } \llbracket \mathbf{exp} \rrbracket_{S, S_{|p, \tau}}^{\tau} ⋇ \eta \\ F & \text{otherwise,} \end{cases} $$

where CI$_{exp}$ is the confidence interval on the evaluation of $\llbracket \mathbf{exp} \rrbracket_{S, S_{|p, \tau}}$ with respect to the chosen coverage probability, and $S_{|p, \tau}$ is the evolution sequence obtained by applying the perturbation p to S at time τ:

$$ (S_{|p, \tau})^t = \begin{cases} S^t & \text{if } t < \tau, \\ S_{S^t}^{p, t-\tau} & \text{if } t \ge \tau. \end{cases} $$

Hence, for the first τ − 1 steps $S_{|p, τ}$ is identical to S. At time τ the perturbation p is applied, and the distributions in $S_{|p, τ}$ are thus given by the perturbation via p of the evolution sequence having S$^τ$ as initial distribution (cf. Definition 4).

**Examples** We now provide a few examples of the use of RobTL for the specification of robustness properties of the two vehicles from Section 2.1.

**Example 1 (Cyber-physical attacks).** In this example, we use RobTL to express robustness properties against cyber-physical attacks modelled by perturbations. Let us consider an attack on the speed sensor of V2 that consists in diminishing the detected value of the speed, according to a chosen probabilistic offset. This attack aims at inducing sudden accelerations of the vehicle, thus increasing the risk of a collision with V1. Hence, we say that the system is robust against the attack if it can limit the risk of a collision between the two vehicles. Firstly, we model the attack by means of the perturbation $p_{ItSlow} = \mathrm{id} @ 0$; $(p_{slow})^{150}$, where $p_{slow} = \mathrm{slow} @ (\mathrm{TIMER} - 1)$. Perturbation $p_{ItSlow}$ has no effect on the initial step (id@0), then we apply function slow every TIMER steps (slow@(TIMER − 1)), for a total of 150 times. The choice of skipping the initial step, and applying the perturbation only every TIMER steps, is related to the frequency at which the controller checks the value of the speed sensor. (We recall that
perturbations are lists of effects to be applied starting from the current step, which is identified with 0. So @ (TIMER - 1) is a list of length TIMER.) An application of slow to a data state d is given by the following system of equations:

$$ 
\begin{aligned}
v &\sim U(0, \text{MAX\_OFFSET}) \\
\text{fake\_speed} &= \min\{\text{MAX\_SPEED}, \mathbf{d}(\mathbf{p\_speed\_V2}) - v \cdot \mathbf{d}(\mathbf{p\_speed\_V2})\} \\
\text{fake\_bd} &= \frac{\text{fake\_speed}^2 + (A + B)(A \cdot \text{TIMER}^2 + 2 \cdot \text{fake\_speed} \cdot \text{TIMER})}{2 \cdot B} \\
\mathbf{d}(\mathbf{s\_speed\_V2}) &= \text{fake\_speed} \\
\mathbf{d}(\text{safety\_gap\_V1\_V2}) &= \mathbf{d}(\mathbf{p\_distance\_V1\_V2}) - (\text{fake\_bd} + \text{SAFETY\_DISTANCE}).
\end{aligned}
$$

As a consequence, we have $\mathbf{d}(\mathbf{s\_speed\_V2}) < \mathbf{d}(\mathbf{p\_speed\_V2})$ and an augmented value for $\mathbf{d}(\text{safety\_gap\_V1\_V2})$ (the nominal one is computed by using $\mathbf{d}(\text{braking\_dist\_V2})$ instead of fake\_bd). This tricks the controller of V2 into accelerating (or idling) when it should brake. Hence, attack $\mathbf{p}_{\text{ItSlow}}$ affects the distance between the two vehicles and, thus, the variation in time of variable $\mathbf{p\_distance\_V1\_V2}$. To measure the effects of $\mathbf{p}_{\text{ItSlow}}$ on the system, we evaluate the probability of a collision to occur upon its application. To this end, we can make use of the penalty function

$$ \rho_{\text{crash}}(\mathbf{d}) = \begin{cases} 0 & \text{if } \mathbf{d}(\mathbf{p\_distance\_V1\_V2}) > 0, \\ 1 & \text{otherwise,} \end{cases} $$

and of the distance expression $\exp_{\text{crash}} = G^{[t_1, t_2]} < \rho_{\text{crash}}$ to quantify the maximal probability of a collision along the time interval $[t_1, t_2]$, where the time bounds $t_1, t_2$ are chosen according to the other system's parameters. Then, we express the robustness of the system against attack $\mathbf{p}_{\text{ItSlow}}$ via the RobTL formula

$$ \varphi_{\text{slow}} = \square^{H} \Delta(\exp_{\text{crash}}, \mathbf{p}_{\text{ItSlow}}) \leq \eta_{\text{slow}} $$

where $H = [0, h]$, with $h$ the chosen time horizon, and the threshold $\eta_{\text{slow}}$ represents the maximum acceptable risk of collision.

Similarly, we can model an attack aimed at inducing sudden decelerations of V1 by means of perturbation $\mathbf{p}_{\text{ItFast}} = \text{id} @ 0; (\mathbf{p}_{\text{fast}})^{150}$ where $\mathbf{p}_{\text{fast}} = \text{fast} @ (\text{TIMER} - 1)$, and function fast differs from slow only for the use of variables of V1, and for sign of the offset $v \cdot \mathbf{d}(\mathbf{p\_speed\_V1})$, which is added to $\mathbf{p\_speed\_V1}$.

We can also combine the perturbations above to model an attack on both vehicles: $\mathbf{p}_{\text{comb}} = \text{id} @ 0; (\mathbf{p}_{\text{fast}}^3; \mathbf{p}_{\text{slow}}^3)^{50}$. We can then exploit RobTL to combine various requirements on the behaviour with respect to different attacks, and test elaborate guarantees on the system. For instance, we use the formula $\varphi_{\text{crash}}$ below to test whether it is sufficient for the two vehicles to be robust each against their own attack, to ensure the robustness of the entire system against a combined attack:

$$ 
\begin{aligned}
\varphi_{\text{fast}} &= \square^{H} \Delta(\exp_{\text{crash}}, \mathbf{p}_{\text{ItFast}}) \leq \eta_{\text{fast}} & \varphi_{\text{comb}} &= \square^{H} \Delta(\exp_{\text{crash}}, \mathbf{p}_{\text{comb}}) \leq \eta_{\text{comb}} \\
\varphi_{\text{crash}} &= \varphi_{\text{fast}} \wedge \varphi_{\text{slow}} \implies \varphi_{\text{comb}}.
\end{aligned}
$$
**Example 2 (Collision severity).** In this example, we use RobTL to express robustness against severity of collisions. Assume that, due to some malfunction, the sensors used by V2 over-approximate the distances from both V1 and the static obstacle. This may cause sudden accelerations of V2 and, possibly, a collision. Hence, we want to analyse the severity of potential collisions induced by sensor malfunction. Intuitively, the severity depends on the speed of V2 at collision instant. Hence, we say that the system is robust against sensor malfunction if it can limit the severity of collisions.

Perturbation $p_{ItDistSens} = id@0; (p_{distSens})^n$ allows us to model this malfunction, where $p_{distSens}$ is the perturbation $distSens@(TIMER - 1)$, and function $distSens$ applied to a data state $d$ has the effect given by the following system of equations:

$$ 
\begin{align*}
\text{offset} &\sim U(0, \text{MAX\_DISTANCE\_OFFSET}) \\
\mathbf{d}(\text{s\_distance\_V1\_V2}) &= \mathbf{d}(\text{p\_distance\_V1\_V2})(1 + \text{offset}) \\
\mathbf{d}(\text{s\_distance\_V2}) &= \mathbf{d}(\text{p\_distance\_V2})(1 + \text{offset}) \\
\mathbf{d}(\text{safety\_gap\_V1\_V2}) &= \mathbf{d}(\text{p\_distance\_V1\_V2})(1 + \text{offset}) - \mathbf{d}(\text{required\_dist\_V2}) \\
\mathbf{d}(\text{safety\_gap\_V2}) &= \mathbf{d}(\text{p\_distance\_V1\_V2})(1 + \text{offset}) - \mathbf{d}(\text{required\_dist\_V2})
\end{align*}
$$

By sensing distances greater than the real ones and reading augmented values for both safety\_gap\_V1\_V2 and safety\_gap\_V2, the controller of V2 may opt for accelerating instead of braking. A collision may follow, whose severity can be quantified by the penalty function

$$ \rho_{\text{crash\_speed}}(\mathbf{d}) = \begin{cases} \frac{\mathbf{d}(\text{p\_speed\_V2})}{\text{MAX\_SPEED}} & \text{if } \mathbf{d}(\text{crashed\_V2}) = 0 \text{ and} \\ \min(\mathbf{d}(\text{p\_distance\_V1\_V2}), \mathbf{d}(\text{p\_distance\_V2})) \le 0 & \text{otherwise.} \end{cases} $$

Here, $\mathbf{d}(\text{crashed\_V2}) = 0$ if and only if there was no crash in the past. In that case, it holds that $\min(\mathbf{d}(\text{p\_distance\_V1\_V2}), \mathbf{d}(\text{p\_distance\_V2})) \le 0$ if a collision occurred at the current time step. Then, when a collision occurs, $\rho_{\text{crash\_speed}}$ returns a value in [0,1] expressing the severity of it, whose computation depends on the speed of V2: severity is expressed as the ratio of the speed at the moment of impact, and the maximal speed. The distance expression $\exp_{\text{crash\_speed}} = G^{[t_1, t_2]} < \rho_{\text{crash\_speed}}$ allows us to capture the max given by $\rho_{\text{crash\_speed}}$ in a suitable interval of time. Then, we express the robustness of the system against sensors' malfunction via the RobTL formula

$$ \varphi_{\text{crash\_speed}} = \square^{H} \Delta(\exp_{\text{crash\_speed}}, p_{\text{ItDistSens}}) \le \eta_{\text{crash\_speed}} $$

where the threshold $\eta_{\text{crash\_speed}}$ represents the maximum acceptable collision severity.

# 4 The STARK Tool

In this section, we provide an overview of the tool Software Tool for the Analysis of Robustness in the unKnown environment (STARK). STARK, developed in Java, is a tool supporting specification, analysis and testing of robustness properties of CPSs. A detailed description of STARK together with a video describing the basic features of our
tool is available at http://quasylab.unicam.it/stark/. STARK consists of five modules, *Models*, *Simulation*, *Statistical Model-Checker*, *Specification* and *Front-end*, that are briefly described below.

**Models.** This module provides interfaces and classes that can be used to describe the computational model and the resulting evolution sequence outlined in Section 2, and RobTL formulae discussed in Section 3. Below, we provide a short overview of the available interfaces and classes.

A system is described by the interface SystemState, that provides the methods used by the simulator and the model checker described later in this section. The interface is implemented by the class ControlledSystem that describes a system composed by:

- a DataState, modelling a *data state*;

- a DataStateFunction, describing how the *environment* affects a data state; and

- a Controller, describing the behaviour of the agents in the system.

To describe the behaviour of a system, the class EvolutionSequence is used. This consists of a sequence of samplings containing at the position *i* the set of configurations that are reachable after *i*-steps of computation. Efficient mechanisms have been implemented to generate the elements in an EvolutionSequence only on demand.

To model perturbations (see Definition 3) the interface Perturbation is available. A perturbation can be applied to a SystemState to obtain a PerturbedSystem. Similarly, the same perturbation can be applied to an EvolutionSequence to obtain an instance of class PerturbedEvolutionSequence.

Moreover, to measure the *distance* between two EvolutionSequences, the interface DistanceExpression is available. This is implemented, following the classic *pattern expression*, to mimic the structure of Definition 2. Similarly, to represent the formulae in Definition 5, the interface RobustnessFormula is used.

**Simulation.** This module contains all the interfaces and classes used to generate an EvolutionSequence (or a PerturbedEvolutionSequence), starting from a SystemState. Specifically, we rely on the class SampleSet, that allows us to manage sets of (sampled) system configurations.

We also provide classes to evaluate *penalty functions* from an evolution sequence and to collect statistical information. The classes rely on *The Apache Commons Mathematics*<fnref n="5" />. The simulation process can be performed following either a *sequential* or a *multi-threading* approach. In the second case *Java Concurrency API* and *stream oriented* computations are used to take advantage of the *parallelism* of the hosting architecture.

**Statistical Model-Checker.** This module provides the classes that can be used to check if a given RobustnessFormula is satisfied or not by an EvolutionSequence. Two mechanisms can be used to *measure* the satisfaction of a formula: one based on the classic Boolean semantics, the other based on a *three-valued semantics*. Both the approaches, based on the pattern *visitor* [11], evaluate the satisfaction of the formula by inspecting its syntax structure.

<footnote n="5">⁵ https://commons.apache.org/proper/commonsmath/</footnote>
*Specification.* The STARK Specification Language (SSL) is a domain specific language that permits defining system behaviour and properties. This module provides the classes that can be used to load a SSL model from a file. A SSL *model* consists of:

- a set of *global variables*;

- a set of *components*;

- an *environment*;

- a set of *properties*.

*Global variables* are used to represent value in the data state that are not associated with a specific component and that are not under the direct control of a controller. In our examples these are<fnref n="6" />:

```python
const SAFETY_DISTANCE = 200;
const TIMER = 5;
const MAX_SPEED = 40;

global variables {
    real p_speed_V1 range [0, MAX_SPEED] = 25;
    real p_speed_V2 range [0, MAX_SPEED] = 25;
    ...
}
```

A *component* identifies an agent in the system. It consists of a set of *local variables* and a *controller*. In our running example we have a component for each of the two vehicles, with the following structure:

```python
component Vehicle1 {
    variables {
        real s_speed_V1 range [0, MAX_SPEED] = 25;
        real s_distance_V1 range [0, INIT_DISTANCE_V1] = 10000;
        ...
    }
    controller {
        state Ctrl {
            if (s_speed_V1 > 0) {
                if (safety_gap_V1 > 0) {
                    accel_V1' = A;
                    timer_V1' = TIMER;
                    brake Light_V1' = 0;
                    exec Accelerate_V1;
                } else {
                    accel_V1' = -B;
                    timer_V1' = TIMER;
                    brake Light_V1' = 1;
                    exec Decelerate_V1;
                } else {
                    accel_V1' = N;
                    timer_V1' = TIMER;
                    exec Stop_V1;
                }
            }
            state IDS {
                ...
            }
        }
    }
}
```

<footnote n="6">⁶ Due to a lack of space only a small code snippet is provided. Complete specification is available at http://quasylab.unicam.it/stark/.</footnote>
```c
        ...
    }
    init Ctrl || IDS
}
component Vehicle2 {
    ...
}
```

The *environment* consists of a set of equations describing how variables are changed after one step:

```c
environment {
    timer_V1' = timer_V1 - 1;
    timer_V2' = timer_V2 - 1;
    p_speed_V1' = p_speed_V1 + accel_V1;
    ...
}
```

*Front-end.* In this module all the classes for the user interaction are provided. First of all, a set of utility classes are provided to read/write data in different formats, such as CSV. These classes can be used to perform some analysis on the behaviour of a CPS even if we do not have information on its specification. Indeed, we can collect the observations on the data of the system into a CSV file, build the *observed* evolution sequence from it, and then use the tool (in particular the module for the evaluation of distances) to compare this observed behaviour with an ideal one, or to compare various observed evolution sequences. This means that we can measure the impact of real world uncertainties and perturbations on the behaviour of the system, without having to specify them, i.e., without assuming any information on which data will be manipulated by them, and on how and when such manipulations occur. A *command line interpreter* is also provided to interact with the STARK modules and permits performing all the analyses outlined above. This interpreter can be either used interactively or in a *batch mode* to execute saved scripts.

# 5 The Tool In Action

We now apply STARK to carry out the analysis on our case study discussed in Section 3.

*Example 3 (Cyber-physical attacks, continued).* Consider the formulae $\varphi_{\text{slow}}$ and $\varphi_{\text{comb}}$ from Example 1. In Figure 2 we depict their three-valued evaluations in various situations, using the identifications $\top = 1$, $\bot = 0$, and $\perp = -1$. The plots in the upper part of the figure report the evaluations of $\varphi_{\text{slow}}$, while those in the lower part are related to $\varphi_{\text{comb}}$. We focus only on $\varphi_{\text{slow}}$, as the analysis for $\varphi_{\text{comb}}$ is similar, with the following parameters: $h = 450$, $t_1 = 350$, $t_2 = 450$, $\eta_{\text{slow}} = 0.1$. Hence, we test whether, when applying the attack at any step $\tau \in [0, 450]$, the maximum probability of a collision, computed between steps $\tau + 350$ and $\tau + 450$, is at most 0.1. We used the following parameters: both vehicles start with an initial speed of 25.0 m/s, with V1 at a distance of 10000 m from the obstacle, and V2 at a distance of 5000 m from V1; $A= 1.0 \text{ m/s}^2$, $B= 2.0 \text{ m/s}^2$, $\text{TIMER}= 5$, $\text{MAX_SPEED}= 40 \text{ m/s}$, and $\text{SAFETY_DISTANCE}= 200 \text{ m}$. In each plot, we report the evaluations with respect to three different instances of the
<figure><img src="image_4.png" /><figcaption>Fig. 2: Evaluations of formulae $\varphi_{\text{slow}}$ (top) and $\varphi_{\text{comb}}$ every 10, 30, and 50 steps, and with respect to different offsets ($\text{MAX\_OFFSET} \in \{0.2, 0.3, 0.4\}$).</figcaption></figure>

parameter MAX_OFFSET, namely 0.2, 0.3, and 0.4, used by the perturbations to set the random offset on speed sensors readings. The system is robust against the attacks using MAX_OFFSET= 0.2, and not robust against those using MAX_OFFSET= 0.4 (we postpone the discussion on the evaluation after step 375). In the case of MAX_OFFSET= 0.3 the formulae evaluate to $\mathbb{W}$, since the threshold $\eta_{\text{slow}}$ is included in the 95% confidence intervals on the computation of distances. Although the evaluation gives (mostly) unknown, the intuition is that the system is not robust in this case. In fact, by comparing the plots, we notice that there are certain time steps, like 0, at which the evaluation changes when working with different simulations of the perturbed evolution sequence. This means that the value of $\eta_{\text{slow}}$ (and $\eta_{\text{comb}}$) is in an $\varepsilon$-neighbourhood of the lower bound of the confidence interval, for an $\varepsilon$ close to 0. Hence, a tiny variation in the confidence interval is sufficient to change the evaluation between $\mathbb{W}$ and $\perp$. The plots have been obtained by considering 10 evaluations of the formula, taken, respectively, every 10, 30, and 50 steps, thus giving us a general idea of the potential impact of the attack on the behaviour of the system, at different moments in time. Notice that, if the attack is applied after step 400, then the formula evaluates to $\top$ regardless of the value of the offset. Actually, this holds whenever the attack is applied after step 374. The reason becomes clear when simulating the nominal behaviour of the system: at step 375 variable $p\_\text{speed\_V2}$ assumes value 0. Clearly, the attack has no effect on a stationary vehicle. Similarly, $p_{\text{comb}}$ has no effect whenever applied after step 350. The temporal discrepancy is due to the fact that in $p_{\text{comb}}$ the attack on V2 is delayed by that on V1 that takes 15 steps to be completed (and has no side effects as V1 becomes stationary at step 260). At that point V2 is already too close to V1 to be tricked by the attack.

**Example 4 (Collision severity, continued).** Consider the formula $\varphi_{\text{crash\_speed}}$ from Example 2. In Figure 3 we depict its three-valued evaluation in various situations, using again the identifications $\top = 1$, $\mathbb{W} = 0$, and $\perp = -1$. As in Example 3, the plots have been obtained by considering 10 evaluations of the formula, taken, respectively, every
<figure><img src="image_5.png" /><figcaption>Fig. 3: Evaluations of formulae $\varphi_{crash\_speed}$ every 10, 30, and 50 steps, and with respect to different thresholds $\eta_{crash\_speed} \in \{0.05, 0.1, 0.15\}$.</figcaption></figure>

10, 30, and 50 steps. The plots report the evaluations of the formula with the following parameters: $\tau = 450$, $t_1 = 10$, $t_2 = 400$. Hence, we test whether a malfunction on distance sensors originating at any step $\tau \in [0, 450]$ gives rise to a maximum severity of a collision, computed between steps $\tau + 10$ and $\tau + 400$, of at most $\eta_{crash\_speed}$. We used the same parameters for the initial speeds, distances and acceleration rates as in Example 3. In Figure 3, we report the evaluations with respect to three different instances of $\eta_{crash\_speed}$, namely 0.05, 0.1, and 0.15. If the attack is applied after step 350, then the formula evaluates to $\top$, the reason being that in all simulations of the nominal behaviour of the system, after step 350 V2 is very close to V1 and also the corrupted value of the distance is enough low to induce the controller to keep braking. The system is robust against the malfunction using $\eta_{crash\_speed} = 0.15$, and not robust against that using $\eta_{crash\_speed} = 0.05$. In the case of $\eta_{crash\_speed} = 0.1$ the formulae (mostly) evaluate to $\emptyset$, since the threshold on the severity is included in the 95% confidence intervals that we considered on the evaluation of the distances.

# 6 Concluding Remarks

We have presented STARK, a Java-based tool for the analysis of robustness properties of CPSs operating in the presence of uncertainties and perturbations. The core of STARK is constituted by the evolution sequence model for system behaviour, and the logic RobTL for the specification of temporal properties over distances between evolution sequences, and thus of requirements on system's robustness.

In the literature, we can find several proposals of tools and techniques for robustness testing for systems with a finite/discrete state space (see [16] for a survey). However, evolution sequences (that can be either obtained through the simulation module in STARK, or via direct measurements on the real system) are defined over a continuous state space, in order to avoid the introduction of arbitrary simplifying assumptions on the behaviour of the environment. This means that in STARK we can capture even the slightest modification on behaviour that is induced by the uncertainties.

Moreover, an evolution sequence is a discrete-time version of the cylinder of all possible trajectories of the system, which means that when we check RobTL properties, we do it by taking into account all possible system behaviours. This is a clear distinction with existing model checking tools, in which properties are tested on a single trajectory of the system (see [1, 15, 22]). It will be interesting to see how this feature
will impact the future development of STARK. In fact, we plan to investigate the synthesis of predictive monitors [5] for RobTL specifications, and to add to STARK a module for the verification of robustness properties at run-time. Clearly, although the monitor attached to the system can observe only a single trajectory at run-time, it will need to take into account all possible future behaviours, and thus the evolution sequence, to make its predictions and take decisions. For completeness, we recall that several useful tools for monitoring (spatio-)temporal properties of CPSs have been proposed in classic run-time monitoring (i.e., without predictions) literature (see [2] for a survey). Those tools are based on temporal logics like, e.g., STL [7], MTL [14], or SSTL [26], that specify properties of a single trajectory of the system at a time.

We also plan to apply our framework to the analysis of biological networks. Some quantitative extensions of temporal logics have already been proposed in that setting (e.g. [8, 19, 20]) to capture the notion of robustness from [12] or similar proposals [17]. It would be interesting to see whether the use of RobTL and evolution sequences, and thus of STARK, can lead to new results.

At this stage in its development, STARK is meant to be used in the testing phase of a system. We leave as future work an investigation of its employment in the design phase. We will also study a possible integration of STARK with SCENIC [10], a domain-specific scenario description language that has been recently introduced for the design of Machine Learning-based CPSs. SCENIC allows us to synthetically generate data for training the system against rare events that are quite difficult to obtain from collections of real-world data. It is a probabilistic programming language for the specification of scenes, i.e., configurations of objects and their spatio-temporal features, and scenarios, i.e., a distribution over scenes and the behaviour of the agents operating in them over time. We remark that requirements over system behaviour in SCENIC are specified in MTL, and are therefore tested on a single trajectory of the system at a time.

**Acknowledgements** This work has been supported by the project "Programs in the wild: Uncertainties, adaptabiLiTy and veRificatiON" (ULTRON) of the Icelandic Research Fund (grant No. 228376-051).

**Data Availability Statement**

The artifact is available in the Software Heritage repository:

swh:1:dir:98532d8c770f9d115c692e932869c446417d8b34

**References**

1. Baier, C.: Probabilistic model checking. In: Esparza, J., Grumberg, O., Sickert, S. (eds.) Dependable Software Systems Engineering, NATO Science for Peace and Security Series - D: Information and Communication Security, vol. 45, pp. 1–23. IOS Press (2016). https://doi.org/10.3233/978-1-61499-627-9-1
2. Bartocci, E., Deshmukh, J.V., Donzé, A., Fainekos, G., Maler, O., Nickovic, D., Sankaranarayanan, S.: Specification-based monitoring of cyber-physical systems: A survey on theory, tools and applications. In: Lectures on Runtime Verification - Introductory and Advanced Topics, Lecture Notes in Computer Science, vol. 10457, pp. 135–175. Springer (2018). https://doi.org/10.1007/978-3-319-75632-5_5

3. Castiglioni, V., Loreti, M., Tini, S.: How adaptive and reliable is your program? In: Proceedings of FORTE 2021. Lecture Notes in Computer Science, vol. 12719, pp. 60–79 (2021). https://doi.org/10.1007/978-3-030-78089-0_4

4. Castiglioni, V., Loreti, M., Tini, S.: RobTL: A temporal logic for the robustness of cyber-physical systems. CoRR abs/2212.11158 (2022). https://doi.org/10.48550/arXiv.2212.11158

5. Chen, X., Sankaranarayanan, S.: Model predictive real-time monitoring of linear systems. In: Proceedings of RTSS 2017. pp. 297–306. IEEE Computer Society (2017). https://doi.org/10.1109/RTSS.2017.00035

6. Chong, S., Lanotte, R., Merro, M., Tini, S., Xiang, J.: Quantitative robustness analysis of sensor attacks on cyber-physical systems. In: 26th ACM International Conference on Hybrid Systems: Computation and Control (2023)

7. Donzé, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Proceedings of FORMATS 2010. Lecture Notes in Computer Science, vol. 6246, pp. 92–106 (2010). https://doi.org/10.1007/978-3-642-15297-9_9

8. Fages, F., Rizk, A.: On temporal logic constraint solving for analyzing numerical data time series. Theor. Comput. Sci. 408(1), 55–65 (2008). https://doi.org/10.1016/j.tcs.2008.07.004

9. Fränzle, M., Kapinski, J., Prabhakar, P.: Robustness in cyber-physical systems. Dagstuhl Reports 6(9), 29–45 (2016). https://doi.org/10.4230/DagRep.6.9.29

10. Fremont, D.J., Kim, E., Dreossi, T., Ghosh, S., Yue, X., Sangiovanni-Vincentelli, A.L., Sesha, S.A.: Scenic: a language for scenario specification and data generation. Machine Learning (2022). https://doi.org/10.1007/s10994-021-06120-5

11. Gamma, E., Helm, R., Johnson, R., Vlissides, J.M.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley Professional, 1 edn. (1994)

12. Kitano, H.: Towards a theory of biological robustness. Molecular Systems Biology 3(1), 137 (2007). https://doi.org/10.1038/msb4100179

13. Kleene, S.C.: Introduction to Metamathematics. Princeton, NJ, USA: North Holland (1952). https://doi.org/10.2307/2268620

14. Koymans, R.: Specifying real-time properties with metric temporal logic. Real Time Syst. 2(4), 255–299 (1990). https://doi.org/10.1007/BF01995674

15. Kwiatkowska, M.Z., Norman, G., Parker, D.: Stochastic model checking. In: Proceedings of SFM 2007. Lecture Notes in Computer Science, vol. 4486, pp. 220–270 (2007). https://doi.org/10.1007/978-3-540-72522-0_6

16. Micskei, Z., Madeira, H., Avritzer, A., Majzik, I., Vieira, M., Antunes, N.: Robustness testing techniques and tools. In: Resilience Assessment and Evaluation of Computing Systems, pp. 323–339. Springer Berlin Heidelberg (2012). https://doi.org/10.1007/978-3-642-29032-9_16

17. Nasti, L., Gori, R., Milazzo, P.: Formalizing a notion of concentration robustness for biochemical networks. In: Proceedings of STAF 2018. Lecture Notes in Computer Science, vol. 11176, pp. 81–97 (2018). https://doi.org/10.1007/978-3-030-04771-9_8

18. Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer (2018). https://doi.org/10.1007/978-3-319-63588-0

19. Rizk, A., Batt, G., Fages, F., Soliman, S.: A general computational method for robustness analysis with applications to synthetic gene networks. Bioinform. 25(12) (2009). https://doi.org/10.1093/bioinformatics/btp200
20. Rizk, A., Batt, G., Fages, F., Soliman, S.: Continuous valuations of temporal logic specifications with applications to parameter optimization and robustness measures. Theor. Comput. Sci. 412(26), 2827–2839 (2011). https://doi.org/10.1016/j.tcs.2010.05.008

21. Rungger, M., Tabuada, P.: A notion of robustness for cyber-physical systems. IEEE Trans. Autom. Control. 61(8), 2108–2123 (2016)

22. Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Proceedings of CAV 2005. Lecture Notes in Computer Science, vol. 3576, pp. 266–280 (2005). https://doi.org/10.1007/11513988_26

23. Shahrokni, A., Feldt, R.: A systematic review of software robustness. Information and Software Technology 55(1), 1–17 (2013). https://doi.org/10.1016/j.infsof.2012.06.002

24. Sontag, E.D.: Input to State Stability: Basic Concepts and Results, pp. 163–220. Springer Berlin Heidelberg (2008). https://doi.org/10.1007/978-3-540-77653-6_3

25. Vaserstein, L.N.: Markovian processes on countable space product describing large systems of automata. Probl. Peredachi Inf. 5(3), 64–72 (1969)

26. Vissat, L.L., Loreti, M., Nenzi, L., Hillston, J., Marion, G.: Analysis of spatio-temporal properties of stochastic systems using TSTL. ACM Trans. Model. Comput. Simul. 29(4), 20:1–20:24 (2019). https://doi.org/10.1145/3326168

27. Xiang, J., Fulton, N., Chong, S.: Relational analysis of sensor attacks on cyber-physical systems. In: 34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, June 21-25, 2021. pp. 1–16. IEEE (2021). https://doi.org/10.1109/CSF51468.2021.00035