HW-based Architecture for Runtime Verification of Embedded Software on SOPC systems

International audienceRuntime verification provides a theoretical provedframework to synthesize monitors from formal specifications.At runtime, these monitors can be used to check that theexecution of the system does not violate a security policy ora safety property. In this paper, we focus on the runtimeverification of safety properties of real-time embedded software.For these systems, it must be ensured that monitoring does notjeopardize the scheduling. To do so, we use a hybrid hardwaresoftwareapproach in the context of System-on-Programmable-Chip. A minimal instrumentation is added to the software toextract the execution trace. The verification is performed byhardware monitors on the FPGA. This implementation makesit possible to obtain a temporal overhead almost as low asa hardware implementation while allowing the use of efficientoff-the-shelf platforms. The paper describes the architecture, itsimplementation, and shows results on a realistic case study