PhD seminar - Samaneh Navabpour

Candidate

Samaneh Navabpour

Title

Time-triggered Verification of Real-time Embedded Systems

Supervisor

Fischmeister, Sebastian

Abstract

In safety-critical real-time embedded systems, correctness is of primary concern, as even small transient errors may lead to catastrophic consequences. Due to the limitations of well-established methods such as verification and testing, recently runtime verification has emerged as a complementary approach, where a monitor inspects the system to evaluate the specifications at run time.

In this talk, I will present our novel time-triggered method for runtime verification, where the monitor does not interfere with the timing characteristics of the embedded system. This monitor polls the system state at fixed time periods to evaluate a set of properties.

The main challenge in implementing such a monitor is achieving sound verification. To this end, we have combined static analysis techniques such as symbolic execution with integer programming, genetic algorithms, and graph-theoretic heuristics to minimize the monitoring overhead while ensuring sound verification for resource restrained real-time embedded systems. Our techniques can also be deployed on component-based multi-core real-time embedded systems. Numerous experiments show that our approach not only ensures bounded and predictable sound runtime verification, but it also imposes less overhead in comparison to mainstream runtime verification techniques.