Patent Document ID: 9043746
Application ID: 13041462

Base Claim:
1. A method comprising: representing an event processing application as an event processing network, being a graph with event processing agents as nodes; generating a finite state machine based on the event processing network, wherein the finite state machine is an over-approximation of the event processing application; expressing stateful rules and policies that are associated with the event processing application using temporal logic, to yield a temporal representation of the event processing application; combining the temporal representation and the finite state machine into a model; generating a statement associated with at least one user-selected verification-related property of the event processing application, wherein the statement is generated using the temporal representation; and applying the statement to the model, to yield an indication for: (i) a correctness of the statement or (ii) a counter example, respectively, wherein at least one of: the representing, the expressing, the combining the generating, and the applying is carried out by at least one processor, wherein the at least one verification-related property of the event processing application is a mutual exclusivity of two of the event processing agents within the graph, and wherein the statement indicates that the two or more of the event processing agents are mutual exclusive such that for any given input, one of the two event processing agents produces a different output from another one of the two event processing agents, at a same point of time, and wherein the counter example is compilable into a sequence of events that contradicts the statement.

---

Claim 5:
5. The method according to claim 1 , wherein the at least one verification-related property of the event processing application is reachability of a specified event processing agent within the event processing network, and wherein the statement indicates that the specified event processing agent is unreachable over the graph, and wherein the respective counter example is compilable into a sequence of events that traces a path over the event processing network to the specified event processing agent.