Title :
A Tool for the Automatic Verification of BPMN Choreographies
Author :
Solaiman, Ellis ; Wenzhong Sun ; Molina-Jimenez, Carlos
Author_Institution :
Sch. of Comput. Sci., Newcastle Univ., Newcastle upon Tyne, UK
Abstract :
The Business Process Model Notation (BPMN) provides a standard graphical language that can be used by business analysts for modeling business process choreographies. A challenging task is to formally verify that constructed choreography models are logically correct with respect to safety, liveness, and various application-specific correctness requirements. To aid with this important task, we present a model checker based framework to automate the verification process. The main component of our framework is the BPMN verifier, a tool that can automatically convert BPMN choreography models into PROMELA, the input language of the SPIN model checker. We describe the implementation and functionality of the BPMN verifier, and how the tool eases the task of expressing Linear Temporal Logic (LTL) correctness requirements, through its LTL Manager component.
Keywords :
business data processing; formal verification; BPMN; BPMN choreographies; LTL manager component; PROMELA; SPIN model checker; automatic verification; business analysts; business process choreographies; business process model notation; graphical language; linear temporal logic; verification process; Analytical models; Contracts; Java; Radiation detectors; Standards; XML; BPMN; business processes; choreographies; model checking; verification;
Conference_Titel :
Services Computing (SCC), 2015 IEEE International Conference on
Conference_Location :
New York, NY
Print_ISBN :
978-1-4673-7280-0
DOI :
10.1109/SCC.2015.103
