Hardware runtime verification of embedded software in SoPC Article Swipe

View

Related Concepts

computer science field-programmable gate array embedded system software embedded software controller (irrigation) runtime verification instrumentation (computer programming) set (abstract data type) programmable logic controller system on a chip computer hardware formal verification operating system programming language agronomy biology

Dimitry Solet , Jean-Luc Béchennec , Mikaël Briday , Sébastien Faucou , Sébastien Pillement ·

YOU? · · 2016 · Open Access · · DOI: https://doi.org/10.1109/sies.2016.7509425 · OA: W2464018720

This paper discusses an implementation of runtime verification for embedded software running on a System-on-Programmable-Chip (SoPC) composed of a micro-controller and a FPGA. The goal is to verify at runtime that the execution of the software on the micro-controller conforms to a set of properties. To do so, a minimal instrumentation of the software is used to send events to a set of monitors implemented in the FPGA. These monitors are synthesised from a formal specification of the expected behavior of the system expressed as a set of past-time linear temporal logic (ptLTL) formulas.