[ main page ] [ back ]

32/2012 : Parallel Runtime Verification of Temporal Properties for Embedded Software

RR Number
32/2012
Conference
The 8th IEEE/ASME International Conference on Mechatronic and Embedded Systems and Applications
Author(s)
Thomas Reinbacher, Johannes Geist, Martin Horauer, Andreas Steininger
Abstract
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 favours 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 an automotive window lift system. The parallel framework yields a close to linear speed-up for this use-case when compared to the conventional runtime verification, while the relative area overheads for a multicore implementation remain very moderate.
Bibtex
@INPROCEEDINGS{6275566,
author={Reinbacher, T. and Geist, J. and Moosbrugger, P. and Horauer, M. and Steininger, A.},
booktitle={Mechatronics and Embedded Systems and Applications (MESA), 2012 IEEE/ASME International Conference on}, title={Parallel runtime verification of temporal properties for embedded software},
year={2012},
month={july},
volume={},
number={},
pages={224 -231},
doi={10.1109/MESA.2012.6275566},
ISSN={},}
Download

[ main page ] [ back ]