Event-based characterisation of temporal properties over system states

The design of runtime verification (or monitoring) systems presents a myriad of options — how to instrument properties, in which logic to specify properties, what algorithms to use to implement the property checking, etc. One crucial issue is what elements of the system one is interested in observing, and what points-of-interest one must capture to be able to perform this monitoring. Many runtime verification tools base their properties on the control flow of the system (e.g.): method calls, object creation, exception raising, etc. Especially in the domain of distributed systems, one also finds communication-centric runtime monitoring, in which one focuses on the communication taking place between nodes (e.g. see). Finally, a minority of tools take a data-centric approach, in which one can write properties about the values stored in the system state. The choice of approach has a major influence on how monitoring code can be instrumented in the system. Typically, control-centric approaches use aspect-oriented programming (or similar) technologies to insert additional code identifying the events of interest in the system. On the other hand, to monitor communication in a distributed, message-passing system, one may create communication proxies (actual or local virtual ones) which capture and analyse the messages, i.e. the temporal points-of-interest in such a system. In a data-centric approach, one typically captures points of discontinuity in the values of variables — when they are assigned a value — to be able to capture properties which talk about how the values of the system state changes over time.peer-reviewe