Hardware runtime verification of embedded software in SoPC

International audienceThis paper discusses an implementation of runtimeverification for embedded software running on a System-on-Programmable-Chip (SoPC) composed of a microcontroller anda FPGA. The goal is to verify at runtime that the execution of thesoftware on the microcontroller conforms to a set of properties.To do so, a minimal instrumentation of the software is usedto send events to a set of monitors implemented in the FPGA.These monitors are synthesized from a formal specification of theexpected behavior of the system expressed as a set of past-timelinear temporal logic (ptLTL) formula