AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic

Abstract

We introduce in this paper $\textsc {AMT~2.0}$, a tool for qualitative and quantitative analysis of hybrid continuous and Boolean signals that combine numerical values and discrete events. The evaluation of the signals is based on rich temporal specifications expressed in extended Signal Temporal Logic (xSTL), which integrates Timed Regular Expressions (TRE) within Signal Temporal Logic (STL). The tool features qualitative monitoring (property satisfaction checking), trace diagnostics for explaining and justifying property violations and specification-driven measurement of quantitative features of the signal.

1 Introduction

Cyber-physical systems, such as automotive embedded controllers, medical devices or autonomous vehicles, are often modeled and analyzed by simulation. Simulators generate traces admitting real values often interpreted as continuous-time signals. To evaluate the system under design, these traces are inspected for satisfying some correctness requirements and are often subject to quantitative analysis based on recording some values in certain segments of the signal and performing some computation (summation, minimum) on them.

Over the past decade an extensive framework has been developed whose goal was to bring automated support for this tedious and error-prone task, centered around Signal Temporal Logic (STL) [18, 19]. STL extends the classical LTL in two directions: it uses predicates over real-valued variables in addition to atomic propositions, and it is defined over dense continuous time accessed symbolically with timed modalities as in Metric Temporal Logic (MTL) [17]. This framework, which was initially accompanied by a rudimentary prototype tool [20], had a lot of reported applications in domains such as automotive, robotics, analog circuits, systems biology. It can be viewed as an extension of runtime verification toward cyber-physical hybrid systems. Interested readers may consult the survey in [7].

In this article we present AMT 2.0, a new version of the tool. The new version is much more mature in terms of software engineering aspects such as rigorous typing of signals and properties, introducing programming language features that include declarations and aliases, improvement of the graphical editors, systematic software testing, etc. Furthermore, its functionality has been extended significantly by incorporating several new research results obtained over the last years:

• 1. We combine STL with a fragment of Timed Regular Expressions (TRE) [4, 5], as a complementary formalism to express temporal patterns. The monitoring algorithm for our specification language xSTL thus obtained integrates the recent TRE pattern matching algorithm reported in [22].

• 2. We use the TRE formalism to define segments of the signal to which quantitative measurements should be applied. Thus we obtain a declarative measurement language that does for the quantitative domain what formal specification languages do for correctness checking. The results, first reported in [14], are fully incorporated into the tool.

• 3. We implement the error diagnostics algorithm of [13] which accompanies the report on a property violation with a justification: a small sub-signal (temporal implicant) which is sufficient to imply the property violation and to convince the user of this fact.

With all these features we progress in easing the task of designers who seek to analyze a complex system based on simulations, providing them with an alternative to manual inspection or explicit programming of observers.

The rest of the paper is organized as follows. In Sect. 2 we present the xSTL specification language. Section 3 gives an overview of the tool and its main features. We illustrate the usage of AMT 2.0 in Sect. 4 with two examples. We present the related work in Sect. 5 and give concluding remarks in Sect. 6.

2 Extended Signal Temporal Logic

Extended Signal Temporal Logix (xSTL) essentially combines STL with a variant of TRE. In this section, we provide the mathematical definitions of the specification language.

We denote by $P$ and $X$ finite sets of propositional and data variables, such that $|P|=m$ and $|X|=n$. Data variables are defined over an arbitrary domain $\mathbb {D}$, typically the reals or the integers. We use the notation $w~:~\mathbb {T} \rightarrow \mathbb {D}^n \times \mathbb {B}^m$ to represent a multi-dimensional signal with $\mathbb {T}= [0,d) \subseteq \mathbb {R}$ and $\mathbb {B} = \{ \textsf {true}, \textsf {false}\}$. We denote by ${w}_{p}$ the projection of $w$ on its component p. We denote by $\theta ~:~\mathbb {D}^{n} \rightarrow \mathbb {B}$ a predicate that maps valuations of variables in X into $\{ \textsf {true}, \textsf {false}\}$.

The syntax of an STL formula $\varphi$ with both future and past temporal operators and interpreted over $X\cup P$ is defined by the grammar

where $p\in P$, $x_{1}, \ldots , x_{n} \in X$ and $I \subseteq \mathbb {R}^+$ is an interval. We denote by the until operator that is decorated with an unbounded interval . We use the strict semantics [2] for until and since temporal operators that allows us to define (continuous-time) next and (continuous-time) previous . The instantaneous rise and fall events can be derived using the rules and . We derive other standard operators as follows: $\textsf {true}\equiv p\vee \lnot p$, $\textsf {false}\equiv \lnot \textsf {true}$, $\varphi _1 \wedge \varphi _2 \equiv \lnot (\lnot \varphi _1 \vee \lnot \varphi _2)$, $\varphi _1 \rightarrow \varphi _2 \equiv \lnot \varphi _1 \vee \varphi _2$, , , , and .

The semantics of an STL formula with respect to a signal w is described via the satisfiability relation $(w,t) \models \varphi$, indicating that the signal w satisfies $\varphi$ at time point t, according to the following definition.

We now define a variant of TRE according to the following grammar:

$$\begin{aligned} r := \epsilon ~|~p~|~\theta (x_{1},\ldots ,x_{n})~|~r_{1} \cdot r_{2}~|~r_{1} \cup r_{2}~|~r_{1} \cap r_{2}~|~r^{*}~|~\langle r \rangle _I~|~r_{1} {{\mathrm{?}}}r_{2}~|~r_{2} {{\mathrm{!}}}r_{2} \end{aligned}$$

where I is an interval of $\mathbb R_+$. The semantics of a timed regular expression r with respect to a signal w and times $t \le t'$ in [0, d] is given in terms of a match relation , which indicates that the segment of w between t and $t'$ matches the expression. This relation is defined inductively as follows:

The last two operations associate a pre-condition (resp. post-condition) to the expression. We note that with the pre- and post-condition, we can also syntactically define rise and fall operators by using the rules ${{\mathrm{\uparrow }}}p \equiv \lnot p {{\mathrm{?}}}\epsilon {{\mathrm{!}}}p$ and ${{\mathrm{\downarrow }}}p \equiv p {{\mathrm{?}}}\epsilon {{\mathrm{!}}}\lnot p$. Extended STL specifications require regular expressions to be embedded into STL formulas. We define two operators, begin match (@(r)) and end match ((r)@) that intuitively project any signal segment $(t,t')$ that matches the expression r to its beginning t and its end $t'$, respectively. Thus, xSTL simply extends STL with these two operators:

and with the following semantics

3 Tool Presentation

The AMT 2.0 tool provides for qualitative and quantitative analysis of simulation/measurement traces. Its input consists of two major ingredients. The first is typically a formula or a collection of formulas in xSTL specifying the desired properties (and later measurements) of a continuous signal. The second is a finite representation of the continuous signal. Input signals obtained from simulators or measurement devices are given as finite sequences of time-stamped values of the form $(t_i,w[t_i])$. The tool supports two commonly-used formats: Value Change Dump (vcd) and Comma Separated Values (csv) files. To obtain continuous-time signals, values between sampling points are interpolated inside the tool to yield either piecewise-constant or piecewise-linear signals.

Fig. 1.

AMT 2.0 - an overview of the graphical user interface.

The tool can work either interactively via its graphical user interface (GUI) or, alternatively, in batch mode when we want to monitor against many signals or incorporate monitoring in a more sophisticated analysis procedure that may iterate over behavior-generating models and/or properties in an outer loop. Figure 1 shows the main evaluation window of the GUI which provides two main functionalities: (1) editing xSTL specifications; and (2) launching the monitoring procedure by selecting properties and signals and presenting the outcome graphically. The AMT 2.0 tool is entirely implemented in Java to facilitate its usage across different platforms and operating systems.

The tool supports three main functionalities: (1) qualitative offline monitoring of extended STL specifications; (2) localization and explanation of property violations; and (3) measurements of quantitative features of signals driven by temporal pattern expressed using TRE. In the remainder of the section we present these functionalities in more detail.

3.1 Specifications in AMT 2.0

The tool facilitates specification of xSTL properties in several ways. The GUI provides an xSTL editor, depicted in Fig. 2, with syntax highlighting and line numbering. In addition, the xSTL parser implements a number of features borrowed from programming languages. This includes (1) declaration of variables and constants, (2) parameterized property templates, (3) support for Boolean, real and integer variables and (4) type checking with extensive error reporting.

Fig. 2.

$\textsc {AMT~2.0}$ - xSTL editor.

3.2 Qualitative Monitoring of xSTL

In this section, we sketch the algorithm for the major functionality of the tool, qualitative monitoring of xSTL specifications. The procedure is based on two main methods that we describe in the sequel: the offline marking procedure for STL [19] and the pattern matching procedure for TRE [22].

Fig. 3.

Example of satisfaction signal computation for using back-shifting.

The qualitative monitoring procedure for $\textsc {STL}$ is an offline method that works directly on the input signals. The procedure is recursive on the structure of the specification – it propagates the truth values from input signals via sub-formulas up to the main formula. The algorithm uses the notion of a satisfaction signal – we assign to each sub-formula $\psi$ of $\varphi$ a Boolean signal $w_{\psi }$ such that $w_{\psi }[t] = \textsf {true}$ iff $(w,t) \models \psi$. For each $\textsc {STL}$ operator, we define a method that computes its satisfaction signal from the satisfaction signals of its arguments. For some operators, this computation is trivial. For example, satisfaction signal $w_{\lnot \varphi }$ is obtained by flipping the truth values of the satisfaction signal $w_{\varphi }$. The computation of satisfaction signals for temporal operators is more involved. We give an intuition on the computation of $w_{\psi }$ where and refer the reader to [19] for the technical description of the complete procedure. The computation is based on the following observation: whenever $\varphi$ holds throughout an interval J, $\psi$ holds throughout $(J \ominus I) \cap \mathbb {T}$, where $J \ominus I = \{ t - t'~|~t\in J \; \text {and} \; t' \in I\}$ is the Minkowski difference. Hence, the essence of the procedure is to back-shift (Minkowski difference restricted to $\mathbb {T}$) all the positive intervals in $w_{\varphi }$ and thus obtain the set of time points where holds. This method is illustrated in Fig. 3.

The integration of TRE into the monitoring procedure of xSTL is done in two steps. First, we define the match-set $\mathcal {M}(r,w)$ of a TRE over a signal $w$ as the set of all segments of $w$ that match r, i.e. , and use the algorithm of [22] to compute the match-set. We then use the match begin (@(r)) and match end ((r)@) operators to project the match-sets to satisfaction signals that are then directly integrated into the STL monitoring procedure described above.

Fig. 4.

Example of a match set - (a) p; and (b) $\langle p \rangle _{[1,2]}$.

The algorithm proposed in [22] computes the set of segments of a signal w that match a TRE $\varphi$. Since we are dealing with continuous-time signals, the number of segments is non-countable and so is potentially the number of matches. The algorithm is based on the observation that all those segments can be can be embedded in two-dimensional space, inside the triangle $0\le t \le t'\le |w|$, where a point $(t,t')$ represents the segment starting at t and ending in $t'$. The matching algorithm uses a symbolic representation of the matches as a finite union of two-dimensional zones. Zones are special class of convex polytopes which are defined as the conjunction of inequalities of the form $x_i \prec b_i$ and $x_i - x_j \prec c_{i,j}$, where $\mathord \prec \in \{ <, \le \}$. For instance, the match set $\mathcal {M}(\epsilon ,w)$ for the empty word $\epsilon$ is the diagonal zone $\{(t,t')\in \mathbb {T} \times \mathbb {T}~|~t=t'\}$, while the match for a literal p or $\lnot p$ is a disjoint union of triangles touching the diagonal whose number depends on the number of switching points in ${w}_{p}$. The match set of the time restriction operator is obtained by intersecting the match set with the corresponding diagonal band, hence $\mathcal {M}(\langle \varphi \rangle _I, w) = \mathcal {M}(\varphi ) \cap \{(t,t')~|~t' - t \in I\}$. The match sets for p and $\langle p \rangle _{[1,2]}$ are depicted in Fig. 4. We point the reader to [22] for a complete description of the procedure. The satisfaction signals $w_{@(r)}$ and $w_{(r)@}$ for the match-begin and match-end operators are computed from the match set of r by projecting every $(t,t')\in \mathcal {M}(r)$ on t and $t'$, respectively.

3.3 Trace Diagnostics for STL

The trace diagnostics procedure implements the algorithm presented in [13]. Given an STL formula $\varphi$ and a trace $w$ that violates $\varphi$, the procedure gives an explanation of the fault in the form of a temporal implicant, which is a small sub-signal $w'$ of $w$ which is sufficient to imply violation. In other words, any possible completion of $w'$ into a full signal will violate the property. The diagnostics procedure uses the satisfaction signals computed by the monitoring algorithm from Sect. 3.2 to explain the faults. The method uses the satisfaction explanation operator E (and its dual violation explanation operator F) that for a given formula $\varphi$ returns an implicant of $\varphi$ (respectively of $\lnot \varphi$) which is satisfied by $w$. The explanation operators are defined inductively on the structure of the formula $\varphi$ and on the times t at which explanation of its sub-formulas are required.

We illustrate the idea behind the procedure with the following example. Consider the $\textsc {STL}$ specification , a signal $w$ in which p does not hold during [0, 3) and then holds during [3, 5). It is clear, for instance, that $(w, 0) \not \models \varphi$ and $(w, 3) \models \varphi$. The violation of $\varphi$ by $w$ at time 0 can be explained by the fact that $w$ is continuously false throughout the interval [0, 1]. In other words, we have that $F(\varphi , w, 0) = \bigwedge _{t \in [0,1]} (w_{p}[t] = \textsf {false})$. In contrast, the value of $w$ at any time $t \in [3,4]$ is sufficient to explain the satisfaction of $\varphi$ by $w$ at time 3. Thus $E(\varphi , w, 3)$ could be any $(w_{p}[t]= \textsf {true})$ such that $t \in [3,4]$. We use the notion of a selection function to choose one explanation when there are many possible ones. The full algorithm is described in [13].

3.4 Specification-Driven Measurements

In this section, we present a simple declarative measurement specification language [14] built on top of TRE. The idea is to require the signal segments over which measurements should be taken to be those that match some pattern specified by an expression. An example of a measurement is the time elapsed between the beginning and end of some activity, or the total fuel consumption in a segment where the acceleration pedal is continuously on until the velocity crosses some threshold.

We first recall that the match set of a TRE defines all the trace segments that match the expression, and the number of those can be uncountably infinite. However if we restrict ourselves to patterns that are delimited by instantaneous discrete events, we will have only finitely many matches. Formally, we use the following sub-class of expressions. An event-bounded TRE (e-tre) is an expression of the form

$$ \hat{r}:= {{\mathrm{\uparrow }}}p~|~{{\mathrm{\downarrow }}}p~|~\hat{r}_1 \cdot r \cdot \hat{r}_2~|~\hat{r}_1 \cup \hat{r}_2~|~\hat{r}_1 \cap r $$

with p a proposition, and $\hat{r}_1, \hat{r}_2$ event-bounded TREs.

The measure patterns defining the segments to be measured are of the form $\alpha {{\mathrm{?}}}\psi {{\mathrm{!}}}\beta$, where $\psi$ is the main pattern, and $\alpha$ and $\beta$ are, respectively pre- and post-conditions. The main pattern $\psi$ specifies the portion of the signal over which the measure is taken. To guarantee a finite number of matching segments, $\psi$ is restricted to be an e-tre while $\alpha$ and $\beta$, which can be used to define additional constraints, are TREs.

Given a measure pattern $\varphi$ and a signal w, we first compute all the segments of $w$ that match $\varphi$. We then apply a measuring operator that collects specific signal values over the matched segments. A measure is written with the syntax $\mathrm {op}(\varphi )$ with $\mathrm {op} \in \{ \textsf {time}, \textsf {value}_x, \textsf {duration}, \textsf {inf}_x, \textsf {sup}_x, \textsf {integral}_x, \textsf {average}_x \}$. We finally aggregate the specific measures and provide to the user the minimum, maximum and average measured value, as well as a histogram that summarizes the measurements.

We illustrate specification-driven measurement with an example from the DSI3 automotive communication protocol [16]. The micro-controller and the sensors that use the protocol, communicate by sending analog pulses during the protocol initialization phase. The standard describes the acceptable shapes and duration of such pulses. Figure 5 depicts the specification of a discovery response pulse from the DSI3 standard. In particular, the standard defines the relevant thresholds (2IResp and IResp) which are used to describe the shape, as well as the acceptable duration of the pulse’s ramp ($t_{1}$) and its total duration ($t_{2}$).

To define the pulse pattern we first define the following predicates:

$$ \begin{array}{lllll} i_{h} \equiv i \ge 2IResp &{} ~~ &{} i_{b} \equiv IResp \le i< 2IResp &{} ~~ &{} i_{l} \equiv i < IResp \\ \end{array} $$

and then let

$$\varphi = i_{l} {{\mathrm{?}}}{{\mathrm{\uparrow }}}(i_{b}) \cdot i_{b} \cdot i_{h} \cdot i_{b} \cdot {{\mathrm{\downarrow }}}(i_{b}) {{\mathrm{!}}}i_{l}.$$

We finally apply the measure operation $\textsf {duration}(\varphi )$ to extract the duration of the segments that match the pulse pattern.

Fig. 5.

Discovery response pulse from DSI3.

4 Examples

In this section, we introduce two running examples that we use to illustrate the features and the functionalities of AMT 2.0. The first example is concerned with a mixed-signal bounded stabilization property and is used to illustrate the qualitative monitoring and trace diagnostics functionalities. The second example demonstrates the measurement functionality as applied to jitter in a digital clock.

4.1 Mixed-Signal Bounded Stabilization

Informal Requirements. This requirement states that after every rising edge of the Boolean $trigger$, the usually-stable analog signal $var$ is allowed to oscillate under the following conditions:

• 1. $var$ must always remain below 5 V; and

• 2. $var$ must within 600 s go below 0.2 V, and continuously remain under that threshold for at least 600 s.

Simulation Traces. We evaluate this requirement on 5 different simulation traces. Figure 6 depicts the Boolean $trigger$ signal, as well as the 5 traces named $var0$ to $var4$. We can already reason informally about the satisfaction of the bounded stabilization property by these traces:

Fig. 6.

Bounded stabilization - input signals.

• 1. Trace $var0$ violates the specification because the signal never stabilizes, i.e. it continues oscillating until the end of simulation;

• 2. Trace $var1$ satisfies the specification - the signal always remains smaller then 5 V, and it goes below 0.2 V within 600 s, continuously remaining below that threshold until the end of the simulation;

• 3. Trace $var2$ violates the specification because the signal exceeds 5 V;

• 4. Trace $var3$ violates the specification because the signal does not stabilize below 0.2 V within the specified period; and

• 5. Trace $var4$ violates the specification because of the 3 glitches that occur towards the end of the simulation.

Formal Specification in xSTL. To define the property we first declare the Boolean variable $trigger$, as well as the real variables $var0$ to $var4$. We also declare two constants $vh$ and $vl$, representing the 5 V and 0.2 V thresholds, respectively. We note that we are evaluating the same formula over different signals. Hence, we define a generic property template $stab$ for the bounded stabilization formula, which is the conjunction of conditions (1) and (2) of the informal requirements. The first conjunct says that the real-valued signal must be smaller than 5V. The second conjunct is a conditional formula that uses logical implication. It says that whenever the $trigger$ signal is on its rising edge, the x signal must go below 0.2 V within 600 s and continuously remain below that threshold for at least 300 s. Then each assertion is an instantiation of the template with one of the signals $var0$ to $var4$.

Qualitative Monitoring of the Specification. We illustrate the qualitative monitoring of the property applied to the traces as done using the GUI of the tool. In the evaluation configuration window, we first specify the xSTL specification, the simulation traces and an optional alias file. In addition to setting up the inputs, we also select the representation of the real numbers, the interpolation and the feature of the diagnostics module.

After evaluating the specification on the traces, we can visually depict the results, as shown in Fig. 1. The nodes in the xSTL parse tree view are expandable via a double click. By expanding the node of the specification, we can see that assertion two is satisfied, while assertions one, three, four and five are violated. We note that we can visualize the satisfaction signals for any sub-property of the specification.

Fault Explanation. The fault explanation is given in the form of temporal implicants which are (small) sub-segments of the input signals which are sufficient to imply the property violation. Figure 7 illustrates the visual output of the diagnostics procedure in AMT 2.0 for the bounded stabilization specification. The first two figures show the trace diagnostics report for the third assertion. We can see that the trigger signal does not contribute to the fault, but var3 does at a single point in time within the interval [100, 150]. At that time, var3 is greater than the invariant threshold 5 V which explains the property violation. The last two figures show that same report, but for the fifth assertion. In this case, the fault is explained by the fact that signal trigger gets high at time 100 and by the values of signal var4 at times 350, 600 and 750. We can see that the last two times coincide with the glitches, thus witnessing that var4 never continuously holds below 0.2 V for at least 300 time units.

Fig. 7.

Bounded stabilization - fault explanation.

We note that the tool computes the fault explanations in a hierarchical manner, following the parse tree of the formula. This additional and complementary information can be quite useful in understanding the fault. We finally note that the trace diagnostics can be made hierarchic.

4.2 Digital Clock Jitter

Informal Requirements. Given a continuous-time Boolean-valued signal $clock$, a clock period is defined as a segment that starts with the rising edge of the $clock$ and ends with its consecutive rising edge. The measurement specification is to measure the duration of all the clock periods matched within the $clock$ signal in order to assess the clock jitter.

Simulation Trace. We apply the specifications to a Boolean $clock$ signal, see Fig. 8.

Fig. 8.

Digital clock jitter - a segment of the input signal.

Formal Specification in xSTL. We now formalize the measurement specification for the digital clock jitter analysis in xSTL. We first declare the Boolean variable $clock$, as well as its negation $nclock$. We then specify the pattern $clock\_period$ that consists of concatenations that starts with the rising edge of $clock$ ($start{clock}$), followed by an interval of positive duration where $clock$ holds, followed by another interval of positive duration where $nclock$ holds, and ending with the next rising edge of $clock$. Finally, we declare the actual measurement to be taken as $duration(clock\_period)$ which extracts the durations of all signal segments that match the $clock\_pattern$ pattern.

Pattern-Driven Measurements. The visualization of the measurement specification consists of a histogram depicting the distribution of the measures taken over signal segments that match the pattern, the total number of matched segments, as well as the minimum, maximum and average value of the measures. The visual summary of the clock jitter measurement is shown in Fig. 9.

Fig. 9.

Digital clock jitter - measurements.

5 Related Work

Breach [11] is a MATLAB/Simulink toolbox that enables various types of STL specification analysis. In particular, Breach supports falsification-based testing, parameter synthesis and requirement mining of STL properties. S-TaLiRo [3] is another Simulink/MATLAB toolbox for different robustness analysis of MTL specifications. It provides support for falsification-based testing, parameter mining, runtime verification, conformance testing, computing the worst expected robustness for stochastic systems and debugging of formal requirements. The ViSpec [15] tool, associated with S-TaLiRo, allows visual specification of MTL requirements. BIOCHAM [10] is a tool for inferring unknown (biological) model parameters from temporal logic constraints. The authors in [9] extend STL with freeze quantifiers that allow them to express oscillatory properties. Similar oscillatory properties of the heart behavior are studied using quantitative regular expressions (QRE) in [1].

Montre [21] is a prototype tool for TRE pattern matching. It provides support for both offline and online matching. AMT 2.0 implements the offline matching algorithms used by Montre and adds a specification measurement language on top of it. Montre does not provide support for STL, monitoring and trace diagnostics.

The combination of STL and TRE was inspired by the Property Specification Language (PSL) [12] and SystemVerilog Assertions (SVA) [23] standards used in the digital hardware verification. Both PSL and SVA use the suffix implication operator to combine temporal logic with regular expressions. In contrast, we define match begin and end operators that give us more freedom to decide whether the begin or the end of an expression match is relevant for the property. The only other work that combines temporal logic and the regular expressions in the context of continuous-time applications is presented in [8], where the authors propose the metric dynamic logic as the specification language for reasoning about time-event sequences.

6 Conclusion

We introduced in this paper the AMT 2.0 tool for qualitative and quantitative analysis of traces coming from cyber-physical systems applications. The tool uses an expressive specification language based on a combination of STL and TRE and admits qualitative monitoring, trace diagnostics and property-driven measurements as its main functionalities. The development of the tool is a continuous work in progress and there is a number of features which are planned to be developed in the near future, in particular solving the inverse problem of finding parameters in a formula template the lead to satisfaction by a given signal or a set of signals [6].