Title :
Verifying Web Services Composition based on LTL and colored Petri Net
Author :
Jihan Zhu ; Kan Zhang ; Guangquan Zhang
Author_Institution :
Sch. of Comput. Sci. & Technol., Soochow Univ., Suzhou, China
Abstract :
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.
Keywords :
Petri nets; Web services; automata theory; graph colouring; program verification; Büchi automata; LTL; Web services composition modeling; Web services composition verification; acceptive language; colored Petri net; model checking; modeling checking technique; online shopping; Analytical models; Automata; Computational modeling; Data structures; Mathematical model; Semantics; Web services; Colored Petri Net; LTL; Web services composition; model checking;
Conference_Titel :
Computer Science & Education (ICCSE), 2011 6th International Conference on
Conference_Location :
Singapore
Print_ISBN :
978-1-4244-9717-1
DOI :
10.1109/ICCSE.2011.6028832
