Complex event processing (CEP) emerged as a paradigm to build systems that
react to situations of interest [
Common CEP applications face high-velocity event streams, which renders
the evaluation of queries a performance bottleneck. Therefore, various algorithms
and architectures for e cient CEP have been proposed in recent years, including
techniques for parallelisation and distribution of query evaluation [
Despite all these advancements, we argue that most of these techniques adopt a pragmatic view|they strive for a technical solution of the issues as they emerge in a speci c application. We therefore advocate the design of formal methods to guide the design and implementation of CEP applications. Speci cally, we suggest to rely on well-established formalisms for concurrent systems to reason about the following aspects of CEP applications: { Query veri cation: Formal analysis may reveal whether a query deployed in a CEP system can match at all, speci cally if event streams satisfy domainspeci c constraints. { Sound parallelisation: Formal analysis may identify non-determinism in query evaluation that is introduced through paralelisation schemes for queries that potentially interact with each other. { Robustness guarantees: Formal analysis may enable conclusions on the errors introduced by out-of-order event arrivals at a CEP system, thereby giving robustness guarantees.
In the light of the above reasoning tasks, we developed a formal model of
CEP applications that is grounded in Petri-nets [
Major challenges in this endeavour, however, have been the integration of the various perspectives of a CEP application in a single model: It requires a comprehensive formalisation of the semantics of event streams, event queries, and evaluation architectures, properly capturing their interplay. For instance, it is not su cient to simply capture that an event occurred, but several modalities have to be encoded on the formal level: An event may have occurred, but may be consumed by a match of an event query and, thus, no longer be available to construct further matches. In such a case, the interplay with common evaluation architectures needs to be taken into account. If an event can be consumed only by a single match of a query, sequential evaluation of various match candidates of a query may lead to a di erent result compared to their concurrent evaluation.
Using our formal model, we are able to approach reasoning on the aforementioned aspects of CEP applications through standard reachability analysis. The question of whether a speci c query can match translates into the common problem of identifying whether a speci c state (i.e., a marking in the Petri-net) can be obtained from the initial state. Based thereon, conclusions can be drawn on the general possibility of generating matches; on the changes in the sets of matches obtained under di erent parallelisation schemes; and on the implications of out-of-order arrivals of events, whether they potentially lead to false positives and false negatives in query evaluation.