Model Checking Airline Tickets Reservation System Based On BPEL

摘要

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.