DocumentCode
3347092
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
fYear
2009
fDate
14-17 Oct. 2009
Firstpage
248
Lastpage
251
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Genetic and Evolutionary Computing, 2009. WGEC '09. 3rd International Conference on
Conference_Location
Guilin
Print_ISBN
978-0-7695-3899-0
Type
conf
DOI
10.1109/WGEC.2009.86
Filename
5402900
Link To Document