Verifying Timed Properties of Programs in IoT nodes using Parametric Time Petri Nets

The analysis of timed properties of programs is a complex task, as it is highly dependent on both the software and the hardware. In this work, we propose a framework for modeling with timed formal models the execution of programs, taking into account the micro-architecture of the machine on which it executes. We model both the program, at the instruction set architecture level, and the hardware, including the processor micro-architecture, using time Petri nets. Our implementation uses the ARM Cortex-M instruction set architecture and a hardware architecture representative of microcontrollers used in IoT nodes. The whole translation is fully automated and allows, starting from binary code, to automatically produce the models usable by the state-of-the-art time Petri net model checker Roméo. In addition, and as a proof of concept, we show how we can check, and enforce to some extent, opacity properties on programs, leveraging the ability of Roméo to verify a parametric timed extension of the classical computation tree logic.