Runtime Monitoring#
Recall from the MLTL formal semantics that we interpret an MLTL formula \(\phi\) over a finite trace (aka computation) \(pi\), and check that \(\pi\) models (satisfies) an MLTL formula \(\phi\), denoted as \(\pi\models \phi\).
R2U2 implements real-time, stream-based runtime verification. So our \(\pi\) consists of the traces of relevant sensor and software values from the (currently running) system. R2U2 answers the question of whether \(\phi\) holds starting from time \(i\), evaluated over computation \(\pi\) and outputs a stream of \(\langle time, verdict\rangle\) pairs, one for every time \(i\). We formally write this runtime verification question as: \(\forall i: \pi, i \models \phi\).
For example, let \(\pi\) be the signals for \(p\) and \(q\):
A timing diagram for a computation \(\pi\) with propositions \(p\) and \(q\). Each propositional variable’s value during the trace is depicted as a line. When the line is high, the proposition is true; when the line is low, it is false.#
Let \(\phi\) be \(\textcolor{red}{\bf \Box_{[0,1]} (p \wedge q)}\)
Then R2U2 will output the following given the computation above (where an empty row means no output occurs).
Current System Time |
R2U2 Output |
|---|---|
0 |
\((\textcolor{red}{false},0)\) |
1 |
|
2 |
\((\textcolor{red}{false},2)\) |
3 |
\((\textcolor{red}{false},3)\) |
4 |
\((\textcolor{red}{false},4)\) |
5 |
|
6 |
\((\textcolor{blue}{true},5)\) |
7 |
\((\textcolor{red}{false},7)\) |
8 |
\((\textcolor{red}{false},8)\) |
9 |
\((\textcolor{red}{false},9)\) |
10 |
\((\textcolor{red}{false},10)\) |
11 |
\((\textcolor{red}{false},11)\) |
12 |
\((\textcolor{red}{false},12)\) |
Notice that at times \(i = 2\) and \(i = 7\) we get two outputs: at time 2 we know that \(\phi\) is false when evaluated from times 1 and 2; at time 7 we know that \(\phi\) is false when evaluated from times 6 and 7. We do not get any output when there is not enough information in the system to know absolutely whether \(\phi\) is true or false.