A LOGIC-BASED METHOD FOR BPMN DIAGRAMS VERIFICATION

In this report we illustrate a method to support the verification of business processes built by using the OMG standard BPMN. Such a standard is gaining a wide acceptance in the business domain, however, the lack of a precise, formally defined semantics leads to ambiguities and problems in the interpretations of the produced diagrams. In this respect, the support provided by the existing tools is not complete nor systematic. The report proposes a systematic method, based on a logic approach, referred to as BPAL, to provide a BPMN diagram the needed formal semantics for analysis and properties verification