Formalization and Model Checking of BPMN Collaboration Diagrams with DD-LOTOS

Abstract

Business Process Model and Notation (BPMN) is a standard graphical notation for modeling complex business processes. Given the importance of business processes, the modeling analysis and validation stage for BPMN is essential. In recent years, BPMN notation has become a widespread practice in business process modeling because of these intuitive diagrams. BPMN diagrams are built from basic elements. The major challenge of BPMN diagrams is the lack of formal semantics, which leads to several interpretations of the concerned diagrams. Hence, this work aims to propose an approach for checking BPMN collaboration diagrams to guarantee some properties of smooth functioning of systems modeled by BPMN notation. The verification approach used in this work is based on model checking techniques. The approach proposes as a first step a formal semantics of the collaboration diagrams in terms of the formal language DD-LOTOS, i.e., a phase of the transformation of collaboration diagrams into DD-LOTOS. This transformation is guided by applying the inference rules of the formal semantics of the DD-LOTOS formal language, and we then use the UPPAAL model checker to check the absence of deadlock, safety properties, and liveness properties.