Formal methods to improve public administration business processes (Q2889178)

The article presents a quality framework and tool chain to ensure that designed business processes meet a set of given quality requirements. The work is motivated by an investigation of business processes from the public sector where it has been found that e-government solutions often fail to meet the needs of their users, because they are designed along the existing paper-based processes. The presented quality framework consists of two main steps: First, business process models that are described in the Business Process Model and Notation (BPMN) standard are mapped to process algebraic descriptions, notably CSP models. Second, a set of predefined quality templates represented as linear temporal logic (LTL) formulas is instantiated for a specific business process. Together, the resulting CSP models and LTL formulas become input into a formal verification tool that checks whether a given business process model satisfies a set of given quality attributes. The quality attributes themselves are derived from requirements in the public sector; however, many of them are also applicable to other domains, because they formalize general requirements such as coordination, sharing, control, transparency, and inclusion.