Event patterns for distributed runtime verification

A fundamental problem in networked embedded systems is to know the runtime behaviour. Especially, the behaviour of self-organizing and adaptive systems is difficult to predict, because of the strong coupling with the environment. Monitoring this at runtime is difficult, because the only access is via the network. However, some properties need to be satisfied irrespective of the situation. Therefore the goal of this thesis is to monitor correctness properties at runtime efficiently. The focus is on temporal and distributed system-level properties. The system is modelled as a network of communicating finite-state machines, that operate asynchronous. Each node produces a stream of locally observable primitive events. High-level knowledge can be obtained by specifying an interest in temporal and distributed patterns in the events. From the specification an event detection tree is generated, which monitors the runtime behaviour by detecting the patterns. We show that event ordering is of fundamental importance for the implementation. To make efficient use of the scarce resources the tree is distributed in the network with a centralized distribution algorithm. A proof-of-concept is developed to evaluate the taken approach. Experiments run on a network of wireless nodes show that the cost of distributed monitoring is lower than when centralized in certain topologies. Simulations show that this is not the case with a random topology. Further, in the experiments only a few seconds delay is measured in the detection process. A limitation of the taken approach is that the unreliability of the network has a negative impact on the performance; missing events is an issue. Finally, the applicability is shown to the verification of an application for structural integrity monitoring.Embedded SystemsEmbedded SoftwareElectrical Engineering, Mathematics and Computer Scienc