Model Checking Airline Tickets Reservation System Based on BPEL
Wei Min Zhao, Rongsheng Dong, Xiangyu Luo, Fang Liu · 2009
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.