Foundations for Change-driven Query-based Runtime Monitoring of Temporal Properties

In model-driven engineering, monitoring the behavior of systems with complex dynamic structures is typically performed via query-based runtime monitoring: a runtime model captures a graph-based snapshot of the system state, and properties of interest are captured as graph queries, which are evaluated over the model online. For temporal properties, history-aware runtime models encode a trace of timestamped snapshots, which is monitored via temporal graph queries. In this case, the query evaluation needs to consider that a trace may be incomplete, thus future changes to the model may affect current answers. In this article, we present the first comprehensive formal treatment of query-based runtime monitoring of temporal properties over runtime models that encode incomplete traces. First, we introduce a query evaluation semantics for a querying approach we previously presented: the previous ( plain ) semantics did not consider incomplete traces and could hence return answers that could be affected by future changes to the model; the novel ( definite ) semantics only returns answers if they are definite, i.e., no future change to the model will affect them. Then, we present a formalization of a technique for the operationalization of temporal queries for both semantics, which allows for incremental and change-driven query evaluation. However, in contrast to the plain semantics, the definite semantics depends on the timestamp of the model and thus must recompute all answers for each model in the trace; hence, the definite semantics disables change-driven evaluation. Finally, we present a variation of the plain semantics that enables the approach to keep to change-driven evaluation while returning definite answers. We evaluate the performance of the presented semantics over two case studies and compare them to the state-of-the-art.