In: Weber, Ehrig, Reisig (Eds.): Proc. of 2nd Int. Coll. on Petri Net Technologies for Modelling Communication Based Systems, pages 179-180. DFG Research Group "Petri Net Technology", September 2001.
Abstract: Workflow technology aims to automate the coordination of long-lived, decentralized business and administration processes;example applications are the processing of insurance claims,or the paper submission and refereeing process for a scientific conference.Despite the great potential of this technology and a large number of commercial products, workflow management systems is still widely perceived as falling short of providing a truly dependable IT infrastructure for mission-critical business procsses.This talk presents steps towards dependable workflow technology with provably correct behavior and exactly-once execution guarantees.The pursued approach comprises the specification, verification, and reliable, distributed execution of workflows based on Harel's state and activity charts. The formal notation of state and activity charts is exploited at three levels. At thespecification level, the formalism enforces precise descriptions of business processes while also allowing subsequent refinements and automatic imports from BPR tools.At the level of verification, state charts are amenable to the efficient method of model checking, in order to verify particularly critical workflow properties. Finally, at the execution level,a state chart specification forms the basis for the automatic generation of modules that can be directly executed in a distributed manner, leveraging state-of-the-art techniques from the OLTP area such as transactional message queues.Within the MENTOR project, funded by the German Science Foundation,a coherent prototype system has been built that comprises all three levels: specification, verification, and reliable,distributed execution. In addition, MENTOR has addressed also the critical issue of how to automatically configure a workflow management system so that it can guarantee meeting application-specified goals for availability, throughput and response time, as well as performability.