| 1. |
- Ericsson, AnnMarie, et al.
(författare)
-
REX, the Rule and Event eXplorer
- 2007
-
Ingår i: DEBS '07. - New York : Association for Computing Machinery (ACM). - 9781595936653 ; , s. 71-74
-
Konferensbidrag (refereegranskat)abstract
- Complex Event Processing (CEP) is a technology with support for matching patterns in a cloud or streams of events in order to support detection of specific combinations of event occurrences. A clever specification of event patterns may, for example, detect fraud attempts in a banking system, fire an alarm in response to hazardous situations in a control system or report suspicious customer behavior.Several CEP engines have support for graphically modelling applications as well as perform tests and provide execution traces to verify the application behavior. We argue that it is beneficial to complement testing with formal verification in order to detect errors in early stages of development.In this paper, we present the research prototype tool REX. REX is built as a loosely coupled front end to the timed-automata CASE tool UPPAAL. CEP applications and application specific properties can be specified in REX. To support formal verification, REX seamlessly transforms the CEP application together with the specified properties to the timed automata CASE tool UPPAAL where the properties are verified by the model-checker provided by UPPAAL.
|
|
| 2. |
- Ericsson, AnnMarie, et al.
(författare)
-
Seamless Formal Verification of Complex Event Processing Applications
- 2007
-
Ingår i: DEBS '07. - New York : Association for Computing Machinery (ACM). - 9781595936653 ; , s. 50-61, s. 50-61
-
Konferensbidrag (refereegranskat)abstract
- Despite proven successful in previous projects, the use of formal methods for enhancing quality of software is still not used in its full potential in industry. We argue that seamless support for formal verification in a high-level specification tool enhances the attractiveness of using a formal approach for increasing software quality.Commercial Complex Event Processing (CEP) engines often have support for modelling, debugging and testing CEP applications. However, the possibility of utilizing formal analysis is not considered.We argue that using a formal approach for verifying a CEP system can be performed without expertise in formal methods. In this paper, a prototype tool REX is presented with support for specifying both CEP systems and correctness properties of the same application in a high-level graphical language. The specified CEP applications are seamlessly transformed into a timed automata representation together with the high-level properties for automatic verification in the model-checker UPPAAL.
|
|
