Verifying Properties of (Timed) Event Driven Process Chains by Transformation to Hybrid Automata

Abstract: Event-driven Process Chains (EPCs) are a commonly used modelling technique for design and documentation of business processes. Although EPCs have an easy-to-understand notation, specifying entire information systems leads to rather large and complex models. Questions like for instance the termination of a process (within some given time)--easy to answer for small EPCs--can hardly be answered for those models. Nevertheless, questions like these can be vital for the execution of the described business processes. Whereas simulation might be able to give a hint on whether the process terminates, only verification can give such guarantees. In this paper we introduce a method to verify properties of what we call Timed EPCs (EPCs annotated with time attributes). We transform Timed EPC to (hybrid) automata and thereby define EPCs formally. Based on the formal definition, properties of EPCs (like e. g. is the ending event always reached within 20 time units) can be verified by transfo...

• Type: Conference
• Year: 2006
• Where: EPK
• Authors: Stefan Denne
• Keywords: Business Processes, Define Epcs, EPK 2006, EPK 2007, Event-driven Process Chains