Resumen
Workflows describe sequences of tasks to achieve goals. These sequences can contain decisions, loops, and parallelisations and are, therefore, similar to computer programs. Experts in the domain of workflow application usually design these workflows. However, these experts are rarely IT experts. For this reason, after automation by a computer, workflows can exhibit undesired behaviors. Such behaviors can be expensive and dangerous and should be avoided. The notion of soundness describes the absence of the undesired behaviors of deadlocks and abundances. The state of the art in workflow verification can detect such behaviors, but gives no indication of causes, does not provide detailed diagnostic information, or is slow. This article introduces two new compiler-based techniques to find causes of deadlocks and abundances. These techniques provide detailed diagnostic information and have a cubic asymptotic complexity of runtime. Their efficiency and quality is evaluated using a benchmark of over thousand real-world workflows together with two leading state-of-the-art approaches.