Title :
Model Checking Airline Tickets Reservation System Based on BPEL
Author :
Wei, Zhao ; Dong, Rongsheng ; Luo, Xiangyu ; Liu, Fang
Author_Institution :
Sch. of Comput. & control, Guilin Univ. of Electron. Technol., Guilin, China
Abstract :
BPEL is a business flow language which describes the composition of web services. Since business flow is very complex, the method of formalized analysis can help ensure the accuracy of composition of web services. For the Airline Tickets Reservation System described by BPEL, we provide a formalized analysis process with FSM in this paper, and finally translate it into programs described by Promela. The safety property and behavior property are verified with model checking tool SPIN, the results of experiment show no flaw in this system.
Keywords :
Web services; formal verification; reservation computer systems; BPEL; FSM; Promela; Web services; airline tickets reservation system; business flow language; model checking; Automata; Formal verification; Genetics; Petri nets; Protocols; Safety; Software design; Software systems; Web services; Writing;
Conference_Titel :
Genetic and Evolutionary Computing, 2009. WGEC '09. 3rd International Conference on
Conference_Location :
Guilin
Print_ISBN :
978-0-7695-3899-0
DOI :
10.1109/WGEC.2009.86
