[Zurück]

T. Reinbacher, J. Brauer, M. Horauer, A. Steininger, S. Kowalewski:
"Runtime verification of microcontroller binary code";
Science of Computer Programming, 80 (2014), S. 109 - 129.

Runtime verification bridges the gap between formal verification and testing by providing
techniques and tools that connect executions of a software to its specification without
trying to prove the absence of errors. This article presents a framework for runtime
verification of microcontroller binary code, which provides the above mentioned link
in a non-intrusive fashion: the framework neither requires code instrumentation nor
does it affect the execution of the analyzed program. This is achieved using a dedicated
hardware unit that runs on a field programmable gate array in parallel to the analyzed
microcontroller program. Different instances of this framework are discussed, with varying
degrees of expressiveness of the supported specification languages and complexity in the
hardware design. These instances range from invariant checkers for a restricted class of
linear template constraints to a programmable processor that supports past-time linear
temporal logic with timing constraints.

http://dx.doi.org/10.1016/j.scico.2012.10.015