Distributed Runtime Verification on Embedded Systems

The author of this thesis is Malte Schmitz.

This thesis analyses and implements modifications of Linear Temporal Logic (LTL) and monitor generation procedures for these logics that can be used for runtime verification of distributed asynchronous embedded systems. For this purpose a distributed temporal logic with past operators (ptDTL) and a distributed temporal logic (fDTL) which is based on the three-valued temporal logic (LTL3) are used. Furthermore a synchronized modification of this logic (fSDTL) is studied. Especially for the three-valued logics new monitor generation procedures using automata models are developed and compared with already known procedures. LEGO Mindstorms robots programmed using the C dialect NXC are used as embedded systems. Within the scope of this thesis a Scala application was developed which performs monitor injection via program transformation. It takes the C source code of multiple robots, parses the annotations contained in comments and adds the routines needed for distributed runtime verification to the source code. Using this software, the different monitor generation procedures and ways of state generation are compared in practice.