A Study in Specification and Hardware Runtime Verification of Critical Embedded Software

We evaluate HARVEST (Hardware Accelerated Runtime Verification for Embedded SofTware), a runtime error detection mechanism for embedded software running on standard SoPC architectures, i.e., one (or more) processor(s) and an FPGA on a single chip. The program under monitoring runs on the processor(s), while a trace analysis module running on the FPGA detects errors in its execution. The hardware implementation of trace analysis minimizes the performanceimpact and achieves a very low error reporting latency (a few processor cycles). In this article, we evaluate the suitability of using HARVEST to detect errors resulting from transient physical faults. We explain how HARVEST is used to monitor a complex software component (Trampoline RTOS) on a commercially available hardware platform (Microchip SmartFusion2). We measure the overhead of the resulting instrumentation on system resources. We then evaluate its performance in detecting silent data corruptions, based on a systematic simulation of bit flips at the instruction set architecture level. We report a detection rate of up to 90.2% for a fairly low system resource overhead, suggesting an interesting trade-off for designers of highly constrained critical systems.