Verification of Event-Driven Process Chain with Timed Automata and Time Petri Nets

Event-driven Process Chain (EPC) is a known business process modeling language which is primarily renowned for efficient modeling of business requirements. It is a semi-formal modeling language which is commonly verified though various formal mechanism for simple atomic events. However, the complexity of business requirements cannot be modeled through EPC atomic events alone especially in case of real time systems. Therefore, the complex events patterns like Event Time, Event location, Event Cardinality, Event Sequence, Event Exclusion, Event Trend and Data dependency are introduced in EPC from the novel area of complex event processing. However, to the best of our knowledge, there is no mechanism available in EPC to model and verify such complex events. Therefore, in this paper, we investigate the verification possibilities of both (atomic and complex) events in the context of Timed-Automata (TA) and Time Petri Nets (TPN). Particularly, we try to map the semantics of simple and complex events with the corresponding concepts of TA and TPN. It is analyzed that the simple EPC events can be formalized through TA and TPN but limited support is available for complex events. The restaurant process case study has been used for further investigation of complex events. It has been concluded that TA formalism is more suitable than TPN for the verification of complex events in EPC.