Parallel runtime verification of temporal properties for embedded software

We present a framework for parallel, non-intrusive runtime verification of past-time linear temporal logic (ptLTL) specifications that follows the trend of contemporary hardware designs which favors an increasing number of computing cores instead of a speedup of a single core. We introduce parallelism by sharing the truth values of common atomic propositions of the specification among multiple, low-hardware footprint micro-CPU cores that evaluate different specification items. The framework is generic and intended to work as an additional runtime verification engine that can be attached to the system under test by wire-tapping its memory interface. For better illustration of the approach we present a case-study where we verify some properties of a finite state machine that models a power windows system. The parallel framework yields a close to linear speedup for this use-case of up to 32 parallel verification units when compared to the conventional runtime verification, while the relative area overheads for a multi-core implementation remain very moderate.