Visual Specification Language and Automatic Checking of Business Process

In this work we propose a visual language for specifying behavioral properties of business processes (BP). We use Business process modeling notation (BPMN) to modelize BP, Petri Net as underlying formal foundations, and SPIN model checker to validate the dynamic behaviors of this process. The objective of this paper is to propose graphical property specification language which can be used during the design phase of BP. The proposed visual language uses the same concepts as established in BPMN to specify the properties to be verified. A semantic interpretation for properties expressed is given based en temporal logic formulas. The advantage of the proposed language is that it hides the temporal logic used for the specification of properties, and the knowledge of this logic is not needed