Monitoring Hybrid Automata
Paul Bungert
Even carefully designed systems can fail due to environmental factors not anticipated at design time. Therefore, verification at the modeling stage is insufficient and needs to be complemented with methods that detect errors while the system is deployed. One technique designed for this task is runtime monitoring. Runtime monitors are deployed alongside systems to determine when predefined properties are violated. A common choice for the specification of monitoring properties are temporal logics, as timing is an important factor in many systems interacting with the real world. However, temporal logics only provide a coarse abstract view of underlying systems. Thus, they cannot cover all monitoring properties and need to be complemented by alternatives. This thesis assesses how hybrid automata can be used for the specification of runtime properties. Originally a modeling tool, hybrid automata are well-suited to capture the complex continuous behavior and structures of systems under scrutiny. We present a monitoring algorithm that decides whether a system trace lies within the trace set of a hybrid automaton specification. The theoretical algorithm is implemented in MATLAB and demonstrated on two case studies.
Bachelor Thesis.