Bringing a high confidence to the validity of business processes is one of the prevailing themes in business process management. Regardless of the introduction of BPMN 1.2, there is no discernible improvement in the preciseness of the BPMN semantics. Motivated by the need to ensure the trustworthiness of BPMN models and the absence of an accurate behavioural semantics, a rigorous semantic definition of BPMN is advocated. The symbolic encodings of the execution semantics are expressed concisely using linear temporal logic (LTL). The LTL-based representations serve as a basis for the formal analysis of BPMN diagrams as well as the prototypical implementation of software tools.
展开▼
