Continuous Correctness of Business Processes Against Process Interference

In distributed business process support environments, process interference from multiple stakeholders may cause erroneous process outcomes. Existing solutions to detect and correct interference at runtime employ formal verification and the automatic generation of intervention processes at runtime. However, these solutions are limited in their generality: they cannot cope with interference that occurs during the entire runtime of the business process, some of which is unknown at design time. In this paper, we present an automated framework for the runtime verification and correction of business processes against interference, which guarantees continuous correctness of process execution in any distributed environment. The continuous detection of interference during process execution is achieved on-the-fly using temporal verification of the running process together with virtual external data transactions, this identifies a minimal set of process checkpoints where the execution of external transactions would change the outcome of the local process. To achieve continuous correction, runtime checks are made at these process checkpoints, and, whenever interference occurs, an intervention process is generated to correct the local process from its current state. Subsequently, any intervention process is itself continuously verified and corrected, thus guaranteeing correct execution throughout the lifetime of a process. The approach is evaluated on a real case-study from the Dutch e-Government.