Towards formal verification of business process using a graphical specification

Bringing a high confidence to the validity of business processes is one of the prevailing themes in business process management. This paper deals with the integration of the formal verification techniques of business process (BP) in the design phase. The main objective of this paper is to propose a user-friendly graphical interface that business experts can use to specify the right dynamic behaviors of BP. In order to achieve this purpose, we use the graphical notation of BPMN (Business process modeling notation) for modeling BP. The graphical interface proposed uses the same notations as those used in BPMN. In this way, the designer can automatically and intuitively validate constraint specifications on designed processes at this early stage. Several formal semantics for these properties are given and a verification approach is then proposed.