Verifying Web Services Composition based on LTL and colored Petri Net
Jihan Zhu, Kan Zhang, Guangquan Zhang · 2011
The main method of model checking based on LTL is constructing a Büchi automata by system model and a Büchi automata equaling with the LTL denied form, and then checking the automata's acceptive language is empty or not. The idea of verifying Web Services Composition is modeling Web Services Composition by Colored Petri Net, and then using the modeling checking technique to verifying the model. It can find the fault occurring in the process of composing Web Services efficiently. Finally, an example of online shopping is used to explain the idea's correctness.