AGH-University of Science and Technology
BPMN is a visual notation for modeling business processes. Although there are many tools supporting it, they rarely provide formal verification of models. The authors propose a new approach to formal verification of BPMN models using the Alvis modeling language and the XTT2 knowledge representation. The structure of the BPMN model can be analyzed using translation to Alvis. Alvis models can be verified with dedicated tools, and their properties can be linked to the properties of the original BPMN model.