DocumentCode :
1671053
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
fYear :
2015
Firstpage :
728
Lastpage :
735
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;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Services Computing (SCC), 2015 IEEE International Conference on
Conference_Location :
New York, NY
Print_ISBN :
978-1-4673-7280-0
Type :
conf
DOI :
10.1109/SCC.2015.103
Filename :
7207421
Link To Document :
بازگشت