Modeling and Formal Analysis of Probabilistic Complex Event Processing (CEP) Applications

摘要

Complex Event Processing (CEP) is a powerful technology used in complex and real-time environments. CEP is an Event Driven Architecture (EDA) style consists of processing different events within the distributed enterprise system attempting to discover interesting information from multiple streams of events in timely manner. In real world, the streams of events are uncertain, which means that is not guaranteed that an event has actually occurred, this uncertainty is due mainly to imprecise content from the event sources (Sensors, RFID,...). As a result, probabilistic CEP has become an important issue in complex environments that require a real-time reaction given streams of probabilistic events. It is evident that building probabilistic CEP applications is not a trivial task, which makes the description of these applications and the analysis of their behavior a necessary task. In this paper, we propose a formal verification approach for probabilistic CEP applications based on probabilistic model checking. To this end, we use the probabilistic Timed Automata (PTA) for describing the probabilistic CEP applications, and the Probabilistic Timed CTL (PTCTL) logic for specifying probabilistic timed properties.