Gregor Gössler

Lȃcrȃmioara Aştefȃnoaei

Blaming in Component-Based Real-Time Systems *

.

Introduction

In component-based real-time systems such as autonomous cars or interconnected medical devices, determining the cause of an observed failure is a pivotal question. Establishing a causal link between the failure of one or more components and the violation of a system-level safety property is instrumental to blame components, be it to issue a precise alert or establish the contractual liability of component providers. However, we currently lack a general framework for blaming in component-based real-time systems.

In this paper, we address this problem by proposing a diagnostic mechanism that relies on counterfactual reasoning ("what would have been the outcome if component C had behaved correctly?") to distinguish component failures that actually contributed to the outcome from failures that had no impact on the system-level failure.

Analyzing causality is a hard task for a couple of reasons: an event e may not directly cause a failure f , but through a causal chain; f may be caused by any of two observed events e 1 and e 2 , or by the conjunction of both. The quest to formalize causality goes back at least to Hume [START_REF] Hume | An Enquiry Concerning Human Understanding[END_REF]: [...] we may define a cause to be an object, followed by another, and where all the objects similar to the first are followed by objects similar to the second. Or in other words where, if the first object had not been, the second never had existed. Following Hume, analyzing causality of an event e is based on counterfactuals, that is, fictious scenarios that resemble the observed scenario, but where e does not happen. We illustrate this idea, and the subtleties in formalizing it, on a simple example. Consider a set of three processes sharing a resource, where mutual exclusion is ensured by time division, as shown in Figure 1. P 1 is required to access the resource within one time unit, P 2 after 3 to 4 time units, and P 3 after at least 7 time units; each process may keep the resource for at most 1 time unit. 1 Let us consider the failure scenario shown in Figure 2(a) where both P 2 and P 3 access the resource early. Intuitively, the early access by P 2 entails a violation of mutual exclusion, whereas the early access by P 3 is not in conflict with any other process. Using the counterfactual approach, we may try to analyze whether the failure of P 2 is a cause for the violation of mutual exclusion, by replacing the trace of P 2 by a correct trace, as shown in Figure 2(b). However, the obtained set of traces is not a valid counterfactual scenario in the sense that the traces are inconsistent: they are not observations of any system execution. This is because the behavior of the resource remains the same, and consequently, there is a mismatch between the unchanged delay of 1 preceding the second access of the resource and the corrected delay of 2 in P 2 .

P 1 1 p! 1 v! 4 1 P 2 1 1 p! v! 4 1 P 3 1 1
4 p! 1 v! resource 1 p? 1 p? v? v? 4 p? 1 v? In this work we introduce the notion of unaffected prefixes, which allows us to take the impact of component failures on other components into account. Based on unaffected prefixes we leverage the definition of necessary causality introduced in [START_REF] Gössler | A general trace-based framework of logical causality[END_REF] in order to formalize blaming in real-time systems. We consider a set of black-box components, each equipped with a specification in the form of a timed automaton. On a given execution trace, causality of the components having violated their specifications is analyzed with respect to the violation of a system-level safety property. As in the setting of timed automata we usually have to cope with an infinite number of counterfactuals, we also propose a symbolic encoding.

The paper is organized as follows. Section 2 reviews related work. Section 3 introduces definitions for handling timed automata and traces. Section 4 formalizes our definition and analysis of logical causality, and proposes a symbolic encoding. In Section 5 we apply the approach to two case studies. Sections 6 concludes.

Related Work

Generally speaking, causality analysis frameworks may take several pieces of information into account: the actual, observed behavior (e.g. execution traces, or inputs and outputs), a causal model of the system, and the expected behavior (in the form of specifications). Most existing approaches consider subsets of these entities. There is no single generally agreed-on definition of causality; rather, several definitions have been proposed to meet different needs.

In Halpern and Pearl's influential structural equations model [START_REF] Halpern | Causes and explanations: A structural-model approach. part I: Causes[END_REF], counterfactual reasoning is used to define actual causality on a model of causal dependencies between propositional variables. However, as their approach requires the structural equations to be given, it cannot be applied to single execution traces of black-box components.

In [START_REF] Gössler | A general trace-based framework of logical causality[END_REF] a language-based framework for causality analysis on execution traces has been introduced. Causality of the failures of components in an index set I for the violation of a system-level property P is analyzed in two steps. First, temporal causality in the sense of Lamport [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] is analyzed by computing the cone of influence spanned by the failures of components in I. Then, logical causality is determined by substituting the cone with the possible correct suffixes of the impacted components. If all obtained counterfactual scenarios satisfy P, the violation of P is blamed on the failures of components in I. Real-time systems can be cast in this framework by modeling time progress as explicit synchronizations between all components. However, the proposed analysis of temporal causality would then compute a cone of influence that grossly over-estimates the actual impact of the component failures, thus leading to false positives.

A causality analysis for real-time systems similar to our framework is presented in [START_REF] Wang | A causality analysis framework for component-based real-time systems[END_REF]. The main difference with respect to the approach we present here is that [START_REF] Wang | A causality analysis framework for component-based real-time systems[END_REF] does not systematically take dependencies between component traces into account. Therefore fault propagation may be under-estimated, resulting in the possibility of inconsistent counterfactual scenarios and hence, false positives by vacuity. To our knowledge, [START_REF] Wang | A causality analysis framework for component-based real-time systems[END_REF] is the only approach to cope with blaming in real-time systems.

In [START_REF] Beer | Explaining counterexamples using causality[END_REF] causality of a vector of boolean signals with respect to the violation of an LTL property is analyzed using a variant of [START_REF] Halpern | Causes and explanations: A structural-model approach. part I: Causes[END_REF]. The approach determines, for each signal, the instants where the signal value is, in some context, a cause for the violation of the property. This technique is limited to synchronous Boolean signals and LTL specifications. [START_REF] Kuntz | From probabilistic counterexamples via causality to fault trees[END_REF] extends the definition of actual causality of [START_REF] Halpern | Causes and explanations: A structural-model approach. part I: Causes[END_REF] to totally ordered sequences of events, and uses this definition to construct from a set of traces a fault tree. Using a probabilistic model, the fault tree is annotated with probabilities. The accuracy of the diagnostic depends on the number of traces used to construct the model.

With the goal of localizing faults in source code, [START_REF] Ball | From symptom to cause: localizing errors in counterexample traces[END_REF] uses model-checking to determine program faults as pieces of code that belong to an error trace but not to any correct trace. Given a counterexample in model-checking, [START_REF] Groce | Error explanation with distance metrics[END_REF] uses a distance metric to determine an explanation of the property violation as the difference between the error trace and a closest correct trace. [START_REF] Wang | Whodunit? causal analysis for counterexamples[END_REF] explains a failed assertion c in a program by computing the weakest precondition of c along a counter-example trace and checking at which point the weakest precondition becomes false. More recently, a gametheoretic approach to locate and fix faults has been proposed in [START_REF] Jobstmann | Finding and fixing faults[END_REF]. Delta debugging [START_REF] Zeller | Why Programs Fail[END_REF] is a technique for automatically isolating a cause of some error in transformational systems where the transformation is a black box on which different inputs can be replayed.

Fault diagnosis (see e.g. [START_REF] Sampath | Diagnosability of discrete-event systems[END_REF]) and fault localization aim at determining what unobservable error events occurred, and where in a system. In contrast, our goal is to establish the existence of a causal chain between observed component failures -that is, errors in the sense of [START_REF] Avizienis | Basic concepts and taxonomy of dependable and secure computing[END_REF] -and a system failure.

Temporal causality in the sense of Lamport [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] determines the set of events in the execution of a distributed system that are known to have been posterior to a given event e, but they are not necessarily caused by e in a logical sense. Finally, there is a large body of work on defining causally consistent operational semantics. Basically, the goal is to provide a constructive way of extending an execution prefix to a possibly infinite run satisfying a set of constraints, see [START_REF] Moy | Arrival curves for real-time calculus: The causality problem and its solutions[END_REF] for an example. Being constructive, these approaches do not rely on counterfactual reasoning.

Preliminaries

We recall the definitions of the timed automata and networks of timed automata (NTA) we use. These are a subclass of the timed automata implemented in Uppaal [START_REF] Behrmann | A tutorial on uppaal[END_REF].

Definition 1 (Timed automaton) A timed automaton is a tuple (L, l 0 , X, inv, ch, Σ, E) where:

• L is a finite set of locations, and l 0 ∈ L is the initial location;

• X is a finite set of clocks;

• inv : L → C assigns an invariant to each location;

• ch is a finite set of channels, partitioned into the set ch s of synchronous channels and the set ch b of broadcast channels;

• Σ ⊆ {c! | c ∈ ch} ∪ {c? | c ∈ ch} ∪ {τ } is a finite action alphabet; • E ⊆ L × (Σ × C × 2 X
) × L is a set of edges labeled with an action, a guard, and a set of clocks to be reset. Edges labeled by c? with c being a broadcast channel have the guard true.

C is the set of clock constraints. A clock constraint is defined by the grammar

C ::= true | f alse | x#c | x -y#c | C ∧ C with x, y ∈ X, # ∈ {<, ≤, =, ≥, >} and c ∈ Z.
Invariants are restricted to constraints of the type x ≤ c.

Definition 2 (Semantics of a timed automaton) The semantics of a timed automaton T = (L, l 0 , X, inv, ch, Σ, E) is given by the labeled transition system (LTS) sem(T ) = (Q, Σ, →, q 0 ) where:

• Q = L × V denotes the states of T;

• q 0 = (l 0 , 0) denotes the initial state of T (we require that inv(l 0 )(0));

• → ⊆ Q × (Σ ∪ R ≥0
) × Q denotes the transitions according to the rules:

-(l, v) d → (l, v + d) if ∀d ′ ∈ [0, d], inv(l)(v + d ′ ) (time progress); -(l, v) a → (l ′ , v ′ ) if there exists a transition l, (a, g, r), l ′ in E such that g(v) ∧ inv(l ′ )(v ′ ) with v ′ = v[r] (action transition).
V is the set of all clock valuation functions v : X → R ≥0 , and 0 is the valuation where all clocks are 0. For a constraint C, C(v) denotes the evaluation of

C in v. The notation v + d represents a new valuation function v ′ defined as v ′ (x) = v(x) + d while v[r] represents v ′ defined as v ′ (x) = 0 if x ∈ r, and v ′ (x) = v(x) otherwise. Definition 3 (Semantics of a NTA) The semantics of a network T = n i=1 T i of n timed au- tomata T i with disjoint sets X i of clocks, sem(T i ) = Q i , Σ i , → i , (l 0 i , 0)
, and channels ch s ∪ ch b , is given by the LTS (Q, Σ, →, q 0 ) where:

• Q = ( l, v) | ∀i = 1, ..., n : (l i , v i ) ∈ Q i ; • Σ = (a 1 , ..., a n ) ∈ Σ ǫ 1 × ... × Σ ǫ n | ∃c ∈ ch s ∃i, j : a i = c! ∧ a j = c? ∧ ∀k / ∈ {i, j} : a i = ǫ ∨ ∃c ∈ ch b ∃i : a i = c! ∧ ∀j = i : a j ∈ {c?, ǫ} ∪ {τ } with Σ ǫ i = Σ i ∪ {ǫ}; • q 0 = (l 0 1 , ..., l 0 n ), 0 ; • → ⊆ Q × (Σ ∪ R ≥0 ) × Q given by: -( l, v) d → ( l, v + d) if ∀i : (l i , v i ) d → i (l i , v i + d) (time progress); 4 -( l, v) τ → ( l ′ , v ′ ) if there exists i such that (l i , v i ) τ → i (l ′ i , v ′ i ) and ∀j = i : (l ′ j , v ′ j ) = (l j , v j ) (internal transition); -( l, v) α → ( l ′ , v ′ ) with α = (a 1 , ..., a n ) if there exist: 1. either a channel c ∈ ch s and indices i, j such that a i = c!, a j = c?, (l i , v i ) c! → i (l ′ i , v ′ i ), (l j , v j ) c? → j (l ′ j , v ′ j ), and ∀k / ∈ {i, j} : (l ′ k , v ′ k ) = (l k , v k ) (synchronization); 2. or a channel c ∈ ch b and an index i such that a i = c!, (l i , v i ) c! → i (l ′ i , v ′ i ), ∀j ∈ J : a j = c? and (l j , v j ) c? → j (l ′ j , v ′ j ), and ∀k / ∈ {i} ∪ J : a k = ǫ and (l ′ k , v ′ k ) = (l k , v k ), where J = {j | ∃l ′′ j , v ′′ j : (l j , v j ) c? → j (l ′′ j , v ′′ j )} (broadcast)
where we write l for the vector (l 1 , ..., l n ), and v i stands for the restriction of v to the domain X i .

The alphabet consists of a set of tuples over the component alphabets, indicating for communications the action of each component, and an internal action τ . The intuition behind Definition 3 is as follows. Time can progress uniformly if all timed automata agree on time progress. Internal τ transitions interleave, resulting in an internal transition of T . Two components may interact with complementary actions over a synchronous channel whenever both components are ready to do so. Whenever a send action on a broadcast channel c is enabled in some component, the broadcast may take place and all components having an enabled c? transition take it simultaneously. The symbol ǫ stands for the absence of a component in a communication over a (synchronous or broadcast) channel.

A timed trace over alphabet Σ is a word in (Σ \ {τ }) ∪ N * 2 . Given a timed trace tr =

α 1 α 2 • • • α k and an index i ∈ N, let tr[1..i] = α 1 α 2 • • • α i and let tr[i] = α i . A run of a timed automaton or network of timed automata with semantics (Q, Σ, →, q 0 ) is a finite sequence of transitions r = (l 0 , v 0 ) α1 → (l 1 , v 1 ) α2 → ... αm → (l m , v m ) such that (l 0 , v 0 ) = q 0 .
= α 1 α 2 • • • of T on Σ k , written π k (tr), is the timed trace of T k obtained by removing all ǫ-symbols in π k (α 1 ) π k (α 2 ) • • • .
Hence, internal actions are unobservable in the projection.

The canonical form of a timed trace tr over Σ, written CF(tr), is obtained by replacing in tr any maximal sub-sequence

d 1 d 2 • • • d m of time delays by a single time delay d 1 + d 2 + • • • + d m ,
and removing all zero delays. Definition 5 (Prefix , ⊓, ⊔) A timed trace tr ′ is a prefix of tr, written tr ′ tr, if there exists an index ℓ such that either CF(tr

′ ) = CF(tr[1..ℓ]), or there exist d 1 , d 2 ∈ N such that tr[ℓ] = d 1 + d 2 and CF(tr ′ ) = CF(tr[1..ℓ -1].d 1 ).
For a set P of prefixes of a given trace let P and P denote the minimal and the maximal element of {CF(w) | w ∈ P } with respect to , respectively. We write tr 1 ⊓ tr 2 for {tr 1 , tr 2 }.

For instance, 1.1.p!.1 2.p!.2.v!;

{1.1, 2.p!.2} = 2; {1.1, 2.p!.2} = 2.p!.2. Next we define a timed automaton that accepts exactly a given timed trace by reaching its final state.

Definition 6 (T ) Let tr be a timed trace over Σ. We suppose w.l.o.g. that tr = d 0 a 1 ...d n-1 a n d n for n ≥ 0 with d i ∈ N and a i ∈ Σ, that is, discrete and time steps alternate. Let nbcr(i) denote the number of receptions on a broadcast channel in a 1 a 2 ...a i (we put nbcr(0) = 0), and let m = n + nbcr(n). We construct a timed automaton T (tr) = (L, l 0 , {x, x ′ }, inv, ch, Σ, E) accepting exactly tr as follows. Let L = {l 0 , ..., l m } with inv(l 0 ) = (x ≤ d 0 ), and E = {(l j-1 , (b j , g j , r j ), l j ) | 1 ≤ j ≤ m}. The invariants and transition labels are defined as follows. For

1 ≤ i ≤ n,
• if a i is a reception on a broadcast channel, we use two subsequent transitions to model its timing:

1. b ki = a i , g ki = true, r ki = {x ′ }, inv(l ki ) = (x ≤ d i-1 ∧ x ′ -x ≤ -d i-1 ); 2. b ki+1 = τ , g ki+1 = true, r ki+1 = {x}, inv(l ki+1 ) = (x ≤ d i ). • Otherwise, b ki = a i , g ki = (x = d i-1 ), r ki = {x}, and inv(l ki ) = (x ≤ d i )
where

k i = i + nbcr(i -1). Let complete T (tr) = (l m , x ≥ d n )
identify the states where tr has been accepted.

Since Uppaal does not support guarded receive transitions on broadcast channels (see Definition 1), we encode such a reception by a sequence of two transitions. In the first transition, an auxiliary clock x ′ is reset to measure the time elapsed since the reception. The invariant of the location between both transitions ensures that only timely broadcasts are accepted. For instance, Figure 3 shows T (tr) for tr = 1.p?.1, where p is a broadcast channel. The encoding of binary synchronization in a single transition is straight-forward. Whether tr ∈ L(T ), for a timed trace tr and a timed automaton T = (L, l 0 , X, inv, ch, Σ, E), can be decided as follows. Let tr ′ be the trace obtained by complementing all synchronizations in tr (that is, substituting c? with c! and vice versa, for each channel c ∈ ch), and let B be the network of timed automata obtained by transforming in T (tr ′ ) T all broadcast channels into synchronous channels. Then, tr ∈ L(T ) iff B |= ∃♦complete T (tr ′ ), that is, if the final state of T (tr ′ ) is reachable in the composition.

Causality Analysis

In this section we define causality of component traces for the violation of a system-level property. A system is specified by a system signature: Definition 7 (System signature) A system signature is a tuple (S, Σ, P) where

• S = (S 1 , ..., S n
) is a tuple of component specifications given as timed automata;

• Σ is the alphabet of n i=1 S i ; • P is a safety property such that L( n i=1 S i ) ⊆ P. The last condition means that property P may be violated only if at least one of the components violates its specification.

For our analysis we suppose the following inputs to be given:

• A system signature (S, Σ, P) with component specifications S = (S i , ..., S n ) over alphabets Σ 1 , ..., Σ n .

• A vector of observed component traces tr = (tr 1 , ..., tr n ) over Σ i that are projections of some system-level trace. In the case where the behavior of two or more components is logged into a common trace, the trace of each component is obtained by projection.

• A set I ⊆ {1, ..., n} of component indices, indicating the set of components to be jointly analyzed for causality. Being able to reason about group causality is useful, for instance, in helping to determine liability of component providers that are responsible for more than one component.

The mere fact that the violation of P is preceded by the violation of a component specification S k , is not sufficient to establish that the latter is a logical cause of the former. Therefore, we will now turn to the formal definition and analysis of logical causality.

A Definition of Logical Causality

Intuitively, in order to verify whether the violations of S i by tr i , i ∈ I, are a cause for the violation of P in tr, we have to identify and remove the effect of these component failures on tr and replace it with behaviors that are consistent with a correct execution of the components in I. The obtained behaviors are called counterfactuals. The violations of S i in tr i , i ∈ I, are a cause for the violation of P if all counterfactual traces are in P, that is, if without those violations, P would have been satisfied. In order to determine and eliminate the impact of component failures on the traces of the remaining components, we first compute the set of prefixes that are unaffected by the failures. The critical prefix cp(tr, S) is the longest prefix of tr that is accepted by S.

We can now define the unaffected prefixes of a log tr with respect to a set I of components as the longest prefixes of tr that could also have been observed if the components in I had satisfied their specifications, and the counterfactuals. Definition 9 (Unaffected prefixes, counterfact.) Given a system signature (S, Σ, P), a vector tr of component traces, and an index set I ⊆ {1, ..., n}, we define the unaffected prefixes of tr as follows. Let

tr 0 i = cp(tr i , S i ) if i ∈ I tr i otherwise
and ∀i = 1, ..., n:

tr * i = tr 0 i ⊓ π i (tr ′ ) | tr ′ ∈ (Σ ∪ N) * ∧ ∀j ∃w ∈ extend L(Sj ) (
C S ( tr, I) = {tr ′ ∈ (Σ ∪ N) * | ∀i : π i (tr ′ ) ∈ extend L(Si) (tr * i )}
be the set of counterfactuals to tr.

Intuitively, the vector of unaffected prefixes tr * i is computed by first removing the incorrect suffixes from tr i , i ∈ I, and then removing suffixes that are infeasible in any system-level trace where each component i starts with tr 0 i . More precisely, tr * i is the longest prefix of tr 0 i that is the projection of some system-level trace tr ′ whose projections are prefixes of the trace extensions. The set of extensions extend L (tr) of a trace tr in L(S j ) is the sub-language of the component specification that starts with tr, or {tr} if tr is not accepted by any run of S j .

P 1 1 p! 1 v! 1 3 1 P 2 1 1 1 p! 3 v! 1 P 3 1 1 1 3
p! 1 v! resource 1 p? 1 v? 1 p? 3 p? v? 1 v? Table 1: Second scenario violating mutual exclusion: both {P 2 } and {P 3 } are causes.

The unaffected prefixes (tr * 1 , ..., tr * n ) are thus constructed as maximal prefixes that could also have been observed if all components in I had behaved correctly, whereas the suffixes s 1 , ..., s nsuch that tr i = tr * i .s i -are impacted by the failures of components in I. The counterfactuals reflect the impact of "undoing" the failures of traces in I. The set of counterfactuals is the set of system-level traces whose projections on the components extend the unaffected prefixes with correct behaviors unless the unaffected prefix is itself incorrect. In particular, C S ( tr, I) contains all system-level traces with projections tr * 1 , ..., tr * n . Example 1 The unaffected prefixes of the traces (tr 1 , ..., tr 4 ) in Figure 2 That is, the set of incorrect suffixes in I is a cause for the violation of P by tr if for any counterfactual trace w -sharing with tr the prefixes that are unaffected by the failures of components in I, and after which no more failures occur -, P would have been satisfied. In other words, the failures of components in I are necessary for the violation of P. Note that P may be satisfied by the unaffected prefixes although its violation may be unavoidable in the sequel (and thus, occur in the counterfactuals). By abuse of language we say that the set of components indexed by I is a cause when their incorrect suffixes are a cause.

Example 2 (Two causes) Applied to our running example and the unaffected prefixes computed in Example 1, Definition 10 determines P 2 to be a cause, whereas P 3 is not. Now consider the modified scenario (tr 1 , tr 2 , tr 3 , tr 4 ) shown in Table 1

Symbolic Analysis

In general there may be an infinite number of counterfactual traces. The next definitions will be useful to symbolically construct counterfactual scenarios and analyze causality.

Computing the unaffected prefixes.

First we define p-refine in terms of timed automata. For the sake of simplicity we assume that the component specifications S i are such that for all observable actions a ∈ Σ i \ {τ } and edges l 1 , (a, g 1 , r 1 ), l ′ 1 and l 2 , (a,

g 2 , r 2 ), l ′ 2 , r 1 = r 2 .
That is, all clock resets are uniquely defined by the action. We thus denote them with r(a).

Definition 11 (p-refine

TA ) Consider a timed trace tr = d 1 a 1 • • • d n ∈ (Σ ∪ N ≥0 ) * with T (tr) = (L 1 , l 0 1 , X, inv 1 , ch, Σ, E 1
) and a timed automaton B = (L 2 , l 0 2 , X, inv 2 , ch, Σ, E 2 ) such that tr ∈ L(B). Let l f 1 ∈ L 1 be the final location of T (tr) and l * 2 ∈ L 2 be the location reached in B after accepting tr. Let p-refine B (tr

) = (L, l 0 1 , X, inv, ch ∪ {link}, Σ, E) where L = L 1 L 2 , ∀l ∈ L : inv(l) = inv 1 (l) if l ∈ L 1 inv 2 (l) if l ∈ L 2 , link is a fresh broadcast channel, E = E ′ 1 ∪ E 2 ∪ {(l f 1 , (link!, x = d n , ∅), l * 2 )}, and E ′ 1 = {(l, (a, g, r ∪ r(a)), l ′ ) | (l, (a, g, r), l ′ ) ∈ E 1 }.
Let complete p-refine (B, tr) be the predicate characterizing the locations in L 2 .

The timed automaton p-refine B (tr) is a refinement of B that accepts exactly those traces accepted by B that start with tr. For instance, Figure 4 shows p-refine B (tr) for tr = 1.p?.1 and B being the shared resource in Figure 1(d). Labeling the link transition with a dummy broadcast rather than with an internal τ -transition helps us to ensure compositionality of the symbolic representation, as will be explained in Section 4.2.2.

Using p-refine B we define a symbolic variant of extend L :

extend B (tr) = p-refine B (tr) if tr ∈ L(B) T (tr) otherwise
where B is a timed automaton. Next we define the feasible prefix of a component trace in a system where all components behave according to given timed automata.

Definition 12 (Feasible prefix FP) For a trace tr of component k and a vector B of timed automata whose composition has alphabet Σ, let

FP k (tr, B) = {tr ⊓ π k (tr ′ ) | tr ′ ∈ (Σ ∪ N) * ∧ ∀i : π i (tr ′ ) ∈ L(B i )} FP k (tr k , B)
is the longest prefix of tr k that is the projection of some trace accepted by n i=1 B i . We can symbolically compute FP k (tr k , B) by determining the longest prefix tr ′ k of tr k for which

T (tr ′ k ) i =k B i |= ∃♦complete T (tr ′ k ).
We are now able to symbolically compute the unaffected prefixes as follows. Let

(tr 0 i , B 0 i ) = cp i , p-refine Si (cp i ) if i ∈ I ∨ tr i ∈ L(S i ) tr i , T (tr i ) otherwise
where cp i = cp(tr i , S i ), and ∀i = 1, ..., n:

tr * i = FP i (tr 0 i , B 0 ) B * i = extend Si (tr * i )
The symbolic computation of tr * i satisfies Definition 9, and we can show that tr * = UP S ( tr, I).

Computing the counterfactuals.

According to Definition 9, the set of counterfactual traces C S ( tr, I) is the set of traces whose projections extend the unaffected prefixes tr * . In order to symbolically represent the set of counterfactual traces, we have to ensure that the composition B = n i=1 B * i of the symbolic models constructed above produces (up to prefix-closure) exactly the counterfactual traces in C S ( tr, I).

In particular, we have to avoid that some timed automaton B i = p-refine Si (tr * i ) that has finished accepting the prefix tr * i is still in the final location of T (tr * i ) while another component j sends on a broadcast channel to which i should be listening, according to S i , after accepting tr * i . To this end we use the possibility of Uppaal to give priority to link (see Definition 11) over all other channels.

Verifying causality.

In order to effectively analyze causality we assume the safety property P to be given as an observer O P , that is, a timed automaton whose only discrete actions are receptions on broadcast channels, with a dedicated location ⊥ indicating that P has been violated. Let

complete = i complete p-refine (B * i , tr * i ) if tr * i ∈ L(B * i ) complete T (tr * i ) otherwise
characterize the set of states of B where all prefixes tr * have been accepted. In order to decide causality according to Definition 10 we have to tell whether every complete trace of B satisfies the property P, which is equivalent to model-checking whether

B O P |= ∃♦(complete ∧ ⊥) (1)
that is, whether no complete execution -whose projections are extensions of the unaffected prefixes, and which is thus a counterfactual trace -violates P.

The reason why we use an observer for P, rather than taking a property in the Tctl fragment that Uppaal model-checks [START_REF] Behrmann | A tutorial on uppaal[END_REF], is that P has to be a property over traces -and thus, refer to occurrences of component actions -, whereas Tctl refers to propositional variables (i.e., states). Observers can, for instance, be constructed from properties in the metric interval temporal logic Mitl [START_REF] Alur | The benefits of relaxing punctuality[END_REF][START_REF] Maler | From mitl to timed automata[END_REF], or written by hand as in our case studies.

Case Studies

We have implemented the symbolic analysis presented in the previous section in the prototype tool LoCA (Logical Causality Analyzer) written in Scala, using Uppaal as a backend. In this section we describe two of our experiments with LoCA. For each experiment, the execution times for constructing the counterfactual model and verifying which component to blame are shown in Table 2. These timings were obtained on an Intel Core i7 with 16 GB RAM running Linux.

The Pacemaker Model

This model is that of a dual chamber implantable pacemaker [START_REF] Jiang | Modeling and verification of a dual chamber implantable pacemaker[END_REF][START_REF] Pajic | From verification to implementation: A model translation tool and a pacemaker case study[END_REF]. It consists of seven components whose specifications are shown in Figure 5: • atrium, modeling random behavior of the atrium chamber of a heart. The model assumes an interval [MinW , MaxW ] = [200ms, 1200ms] between two consecutive events Ain!.

• ventricle, modeling the ventricle chamber, with the same timing assumption. Atrium and ventricle are used as a model of the environment of the pacemaker.

• LRI , for lower rate interval, ensures a maximal interval LRI d = 1000ms between a sensed or paced ventricular event and the next atrial event. Past this delay, an atrial pacing event a p! is delivered.

• AVI , a component ensuring an upper bound of AVI d = 150ms between an atrial event (sensed or paced) and a ventricular event. After an elapsed time of AVI d , a ventricular pacing event v p! is delivered.

• URI , for upper rate interval, ensures a minimal delay of URI d = 400ms between a ventricular event and the next ventricular pacing event by delaying the delivery of v p! by AVI . A broadcast on uri ready signals that the minimal delay has elapsed.

• PVARP (post ventricular atrial refractory period) and VRP (ventricular refractory period) filter out noise and early events.

All channels are broadcast channels. The locations labeled with C are committed, that is, they must be left immediately [START_REF] Behrmann | A tutorial on uppaal[END_REF]. Let us first analyze causality of the incorrect suffix of URI . Figure 7(b) shows the unaffected prefixes UP S ( tr, {URI }) for the violation of S URI . In particular, the early a p! event turns out to be independent of URI 's failure. By constructing the set of counterfactual scenarios, Definition 10 establishes that the incorrect suffix of URI is a not a cause for the violation of P. In contrast, the incorrect suffix of LRI is a cause for the violation of P: without a p! being sent early P would have been satisfied. Thus, only LRI is to blame for the violation of P.

The Temperature Controller Model

This model of a chemical reactor is an adaptation from [START_REF] Alur | The algorithmic analysis of hybrid systems[END_REF]. The system being modeled consists of a controller moving n identical rods in order to maintain the temperature between the bounds tLow and tHigh: when the temperature in the reactor reaches tHigh (resp. tLow ), a rod must be used to cool (resp. heat) the reactor. Once moved, a rod can be moved again only after ctr = tHigh×n units of time. The controller is designed such that the time interval between a cooling and heating is of at most tLow time units. Any violations of this safety property leads to shutdown. Our analysis concentrates precisely on this property. To implement an observer which monitors it, the controller is modeled such that it sends a broadcast doneCool! (resp. doneRest!) to signal when a cooling action (resp. resting) just took place. The interactions between the controller and the rods are implemented by means of synchronous communication on the channels cool and rest. All timed automata are depicted in Figure 8. Compared to the pacemaker model, this model is more regular: there are only two different specifications (one for the controller and one for each of the rods), and their only possible interactions are basically synchronizations on cool and rest. The difficulty here comes more from the possibly great number of rods the controller must interact with. Figure 9(a) shows an excerpt from a log recording the execution of a controller in parallel with 7 rods. The prefix corresponds to observations during the first 14 time units for the values of 6, resp. 3 for tHigh and resp. tLow. Two of the traces of the rods, as well as that of the controller have local violations: the rods send their second cool too early and the controller breaks the timing requirements in its specification. Especially the second delay of 4 time units before a rest action entails the invalidation of the global safety property. Among the three candidates, only the controller and the second rod are causes for the global violation: rod 1 cannot be blamed because in any counterfactual scenario constructed from the unaffected prefixes UP S ( tr, {rod 1 }) in Figure 9(b), the global violation due to the late rest between rod 2 and the controller occurs nevertheless. On the contrary, had either one of rod 2 or the controller behaved correctly, the safety property would have been satisfied.

Conclusion

We have given a formalization of blaming in real-time systems composed of black-box components, and provided a symbolic approach for effective blame assignment. The approach has been implemented and successfully applied to the models of a dual chamber implantable pacemaker and that of a chemical reactor, where the described approach could be used to read out logs periodically and identify the components causing safety hazards. Our work opens several directions for future research. First, we would like to investigate possible applications, in particular, to blame assignment in actual safety-critical systems. We believe that ensuring accountability [START_REF] Küsters | Accountability: definition and relationship to verifiability[END_REF] by construction, that is, the possibility of automatic blame assignment after a system failure, should become a requirement in the design of any safetycritical system. Another application of our approach is in system validation by model-checking or testing where the analysis is applied to (possibly symbolic) counterexample traces.

A first extension we will investigate is the distinction between observable and non-observable events, only the former of which are logged. In particular, whenever component failures are not observable, we have to combine fault diagnosis [START_REF] Sampath | Diagnosability of discrete-event systems[END_REF] and causality analysis.

In closed-loop systems, an alternative behavior of the control part will impact the physical process. Therefore the counterfactual behavior of the former should be propagated through a model of the latter. For the pacemaker example, more realistic models of the heart that could be used for this purpose are [START_REF] Ye | Efficient modeling of excitable cells using hybrid automata[END_REF][START_REF] Chen | A simulink hybrid heart model for quantitative verification of cardiac pacemakers[END_REF], at the price of constructing and verifying counterfactuals in the more expressive framework of (stochastic) hybrid automata. We also intend to study how our observation-based approach can be combined with a model-based approach such as [START_REF] Halpern | Causes and explanations: A structural-model approach. part I: Causes[END_REF] to allow reasoning about white-box systems for which causal models are (partially) available.

Our experimental results are promising. In particular, they suggest that the cost for causality analysis of smaller problems is very reasonable. In order to tackle larger models -where the cost should be dominated by model-checking Equation (1) -, it would be of interest to investigate the use of compositional verification for timed automata [START_REF] Astefanoaei | Compositional invariant generation for timed systems[END_REF].

Figure 1 :

 1 Figure 1: Mutual exclusion example.

  (a) Scenario violating mutual exclusion.

  ? 1 p? v? v? 4 p? 1 v? (b) The trace of P 2 is corrected.

Figure 2 :

 2 Figure 2: A failure scenario and a simple counterfactual scenario. Each line is a component trace; vertical alignments of delays and interactions are added to make the scenario more readable. Substituted suffixes are written in bold.

  The timed trace accepted by r is obtained by removing from α 1 α 2 • • • α m all τ -symbols. Let L(T ) be the set of all timed traces accepted by some run of T . Definition 4 (Projection π) Consider a network of timed automata T i with alphabets Σ i , and let T = n i=1 T i with alphabet Σ. The projection of an action α = (a 1 , ..., a n ) ∈ Σ on Σ k , written π k (α), is the component action a k . The projection of a time delay d is d. The projection of an internal action τ is ǫ. The projection of a timed trace tr

Figure 3 :

 3 Figure 3: Timed automaton recognizing the trace 1.p?.1 by reaching the final state (l2, x = 1).

Definition 8 (

 8 Critical prefix cp) Given a timed trace tr = α 1 α 2 • • • over Σ and a timed automaton S over Σ, let cp(tr, S) = {tr ′ | tr ′ tr ∧ tr ′ ∈ L(S)} be the critical prefix of tr with respect to S.

  tr 0 j ) : π j (tr ′ ) w where extend L (tr) = p-refine L (tr) if tr ∈ L {tr} otherwise and p-refine L (tr) = {tr ′ ∈ L | tr tr ′ }. Let UP S ( tr, I) = (tr * 1 , ..., tr * n ) be the vector of prefixes of tr that are unaffected by the failures of components in I. Let

  (a) with respect to the failures of component P 2 are UP S ( tr, {P 2 }) = (tr 1 , tr ′ 2 , tr 3 , tr ′ 4 ) with tr ′ 2 = 2 and tr ′ 4 = 1.p?.1. On the other hand, for component P 3 we get UP S ( tr, {P 3 }) = (tr 1 , tr 2 , tr ′ 3 , tr ′′ 4 ) with tr ′ 3 = 6 and tr ′′ 4 = 1.p?.1.p?.v?.v?.4. Definition 10 (Causality) Consider a system signature (S, Σ, P) and traces tr = (tr 1 , ..., tr n ) such that ∃w ∈ (Σ ∪ N) * \ P ∀i : π i (w) = tr i , and a subset I ⊆ {1, ..., n} of component indices. The incorrect suffixes of the traces indexed by I are a cause of the violation of the property P if C S ( tr, I) ⊆ P

Proof 1

 1 Our blame assignment is sound and complete: Theorem 1 (Soundness) Each cause contains an incorrect trace. Consider a set I ⊆ {i | tr i ∈ L(S i )}. We show that the set of traces indexed by I is not a cause for the violation of P by tr = (tr 1 , ..., tr n ). If all components in I satisfy their specifications, then (tr * 1 , ..., tr * n ) = UP S ( tr, I) = tr. By the hypothesis of Definition 10 there exists w ∈ (Σ ∪ N) * such that w / ∈ P ∧ ∀i : π i (w) = tr i = tr * i . Thus I is not a cause according to Definition 10. Theorem 2 (Completeness) Each violation of P has a cause. Proof 2 Let I = {i | tr i / ∈ L(S i )}, tr = (tr 1 , ..., tr n ), and (tr * 1 , ..., tr * n ) = UP S ( tr, I). By construction of tr 0 -and thus of tr * -, all traces in tr * are prefixes of the traces in tr and satisfy the component specifications. Since (S, Σ, P) is a system signature and hence L( n i=1 S i ) ⊆ P, and P is prefix-closed, all counterfactual traces satisfying the condition of Definition 10 are in P. Hence, I is a cause for the violation of P by tr.

Figure 4 :

 4 Figure 4: p-refine resource (1.p?.1).

Figure 5 :

 5 Figure 5: The Pacemaker model.Let us consider the failure scenario shown in Fig.7(a). Two of the traces violate their specifications: LRI due to an early atrial pacing event a p!, and URI due to a missing uri ready! event

Figure 6 :

 6 Figure 6: The observer.

  atrium

Figure 7 :

 7 Figure 7: The failure scenario.

Figure 8 :

 8 Figure 8: The temperature controller model and its observer.

Figure 9 :

 9 Figure 9: The failure scenario for the chemical reactor model.

  . P 2 releases the resource late, and P 3 accesses it early. The unaffected prefixes UP S ( tr, {P 2 }) are (tr 1 , tr ′ On the other hand, for component P 3 we get UP S ( tr, {P 3 }) = (tr 1 , tr 2 , tr ′ According to Definition 10, both {P 2 } and {P 3 } are causes: a correct behavior of any of them would have resulted in the satisfaction of P.

	2 , tr 3 , tr ′ 4 ) with tr ′ 2 = 3.p!.1 and tr ′ 4 = 1.p?.1.v?.1.p?.1. 3 , tr ′′ 4 ) with tr ′ 3 = 6 and tr ′′

4 = 1.p?.1.v?.1.p?.3.

Table 2 :

 2 Execution times of the queries on the failure scenario in the pacemaker model (top) and the chemical reactor model (bottom).

	I	construction of model-checking C S ( tr, I) Eq. (1)	cause?
	{LRI }	7.2 s	6.0 s	yes
	{URI }	4.7 s	8 ms	no
	{controller}	4.0 s	108 ms	yes
	{rod 1 }	1.3 s	7 ms	no
	{rod 2 }	2.8 s	7 ms	yes

  11.cool!.3.rest!.cool!.rest! rod 2 7.cool!.rest!.cool!.4.rest!.3 rod 3 14.cool!.rest! rod 4 14.cool!.rest! rod 5 14.cool!.3.rest!.7 rod 6 14.cool!.rest! rod 7 14.cool!.rest! controller 4.cool?.doneCool!.3.rest?.doneRest!.cool?.doneCool!.rest?.doneRest!.cool?.doneCool!.4.rest?.doneRest!. cool?.doneCool!.3.rest?.doneRest!.cool?.doneCool!.rest?.doneRest!.cool?.doneCool!.rest?.doneRest!. cool?.doneCool!.rest?.doneRest!.cool?.doneCool!.rest?.doneRest!.cool?.doneCool!.rest?.doneRest! (a) Traces tr. The first violations of component specifications are underlined. The double underlined delay in the trace of the controller indicates the position where the global violation happens. rod 1 11.cool!.3.rest! rod 2 7.cool!.rest!.cool!.4.rest!.3 rod 3 14.cool!.rest! rod 4 14.cool!.rest! rod 5 14.cool!.3.rest!.7 rod 6 14.cool!.rest! rod 7 14.cool!.rest! controller 4.cool?.doneCool!.3.rest?.doneRest!.cool?.doneCool!.rest?.doneRest!.cool?.doneCool!.4.rest?.doneRest!. cool?.doneCool!.3.rest?.doneRest!.cool?.doneCool!.rest?.doneRest!.cool?.doneCool!.rest?.doneRest!. cool?.doneCool!.rest?.doneRest! (b) Unaffected prefixes UP S ( tr, {rod 1 }).

	rod 1

Integer delays are a realistic assumption since logged events will be time-stamped by some discrete clock.

Acknowledgment The first author thanks Insup Lee and Oleg Sokolsky for their feed-back on an early version of this work and for suggesting the pacemaker as a case study.