1 Introduction
-
Source code instrumentation of high-level languages can only capture events that are accessible from within the instrumented software system. Embedded systems [59] often include both hardware and mechanical parts; events from those might go unnoticed for an instrumenting runtime verification approach.
-
The timing behavior of the SUT is altered by instrumentation [23, 34]. The additional runtime overhead may drastically impact the correctness of a heavy-loaded real-time application with tight deadlines. The same applies to memory consumption of resource constrained systems. The relevance of this argument is supported by the fact that restricted architectures are often used in critical environments[12, 33, 66], such as in nuclear power plants [28] and spacecrafts [30, Chap. 3].
-
Instrumentation may make re-certification of the system onerous (e.g., systems certified for civil aviation after DO-178B [73]).
-
In its present shape, runtime verification often analyzes the correctness of high-level code. However, to show that a high-level specification is correctly reproduced by the target system, it is further necessary to show the correctness of the translation of the high-level code into executable code, i.e., the compiler. Despite recent breakthroughs [52, 53], only few verified compilers are used in practice and flaws introduced by compilers [31, 55, 81] may remain undetected by existing approaches.
-
Instrumentation at binary code level may circumvent the process of establishing correctness of the compiler. However, binary instrumentation is incomplete as long as a sound reconstruction of the control flow graph is not obtained from the binary. Despite being an active area of research [7, 35, 46, 67], generating sound yet precise results remains a challenge.
2 Contributions and roadmap
3 Logics for runtime verification
3.1 Past-time linear temporal logic
3.2 Past-time metric temporal logic
can be expressed in ptMTL. The above property, e.g., can be formalized by:“If the system leaves the idle mode, it has received an according signal in the past 50 clock-cycles.”
3.3 Rewriting past-time metric temporal logic to past-time linear temporal logic
4 Observer design for real-time properties
4.1 Decomposing a specification
4.2 The invariant and exists previously operators
4.3 The invariant and exists within interval operators
4.4 The since within interval operator
4.5 Garbage collection
4.6 Discussion of space and time complexity
5 Mapping the framework into hardware structures
5.1 Interfacing the system under test
5.2 Registers and lists of pairs of time points
5.3 Real-time clock
5.4 Evaluation of atomic propositions
5.5 Runtime observers
5.6 A microcomputer to evaluate ptMTL and ptLTL specifications
-
If φ i is an atomic proposition, instantiate an AtChecker block and add its configuration to C a .
-
If φ i is a ptMTL formula, we instantiate the corresponding observer hardware block, generate the hardware block’s configuration and a native instruction for the μ Spy. We add the configuration to C m and the instruction to Π.
OpCode | Addr. Operand 1 | Addr. Operand 2 | Interval Addr. | List Addr. |
---|---|---|---|---|
5 bit | 2+8 bit | 2+8 bit | 8 bit | 7 bit |
Logic | Operator |
μ
Spy clock cycles |
---|---|---|
Boolean | ¬φ
| 1 |
φ
0•φ
1,•∈{∧,∨} | 1 | |
ptLTL
| ⊙φ
| 1 |
φ
1
S
φ
2
| 1 | |
ptMTL
| 2 | |
4 | ||
φ
1
S
J
φ
2
| 4 |
6 Evaluation
6.1 Simulation results
Signal Name | Unit | Meaning |
---|---|---|
s_clk | RVU | system clock of the RV framework |
s_reset_n | asynchronous reset of the RV framework (AL) | |
s_sut_clk | system clock of the SUT | |
s_rtc_timestamp | RTC | ctr. value of the real-time clock (i.e., time point n) |
s_atomic(0) | SUT | truth value of atomic proposition # 0, σ
0 (AH) |
s_atomic(1) | truth value of atomic proposition # 1, σ
1 (AH) | |
s_atomic(2) | truth value of atomic proposition # 2, σ
2 (AH) | |
s_atomic(3) | truth value of atomic proposition # 3, σ
3 (AH) | |
s_violated | RVU | monitoring output e
n
⊨φ (AH) |
command |
μ
Spy
| instruction (op-code) for the μ
Spy
|
state | state of the fetch stage state machine | |
state | state of the load stage state machine | |
state | state of the calc stage state machine | |
state | state of the write back stage state machine | |
interval_min |
min(J) (in RTC ticks) | |
interval_max |
max(J) (in RTC ticks) | |
sel | List | select the list specified by buffer_nr (AH) |
add_start | add start (
) time point to the list (AH) | |
add_end | add end (
) time point to the list (AH) | |
set_tail | clear list and add new entry (AH) | |
reset_tail | clear list and add entry with time point 0 (AH) | |
drop_tail | remove tail element from the list (AH) | |
delete | remove head element from the list (AH) | |
buffer_nr | id of the currently used list (AH) |