Conducting verification in event processing applications using formal methods

A system comprising:

• a graph builder configured to represent an event processing application as an event processing network, being a graph with event processing agents as nodes;
• a finite state machine generator configured to generate a finite state machine, based on the event processing network, wherein the finite state machine is an over-approximation of the event processing application;
• a logic expresser configured to express 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;
• a combiner configured to combine the temporal representation and the finite state machine into a model;
• a statement generator configured to generate 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
• a model checker configured to apply the statement to the model, to yield an indication for:
• (i) a correctness of the statement or (ii) a counter example, respectively,
• wherein the graph builder, the finite state machine generator, the logic expresser, the statement generator, and the model checker are in operative associated with at least one processor.

A computer program product for applying formal verification methodology to an event processing application, the computer program product comprising:

• a computer readable storage medium having computer readable program embodied therewith, the computer readable program comprising:
• computer readable program configured to represent an event processing application as an event processing network, being a graph with event processing agents as nodes;
• computer readable program configured to generate a finite state machine, based on the event processing network, wherein the finite state machine is an over-approximation of the event processing application;
• computer readable program configured to express 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;
• computer readable program configured to combine the temporal representation and the finite state machine into a model;
• computer readable program configured to generate 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
• computer readable program configured to apply the statement to the model, to yield an indication for:
• (i) a correctness of the statement or (ii) a counter example, respectively.