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

fYear

2011

fDate

3-5 Aug. 2011

Firstpage

1127

Lastpage

1130

Abstract

The main method of model checking based on LTL is constructing a Büchi automata by system model and a Bü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; Bü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;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Science & Education (ICCSE), 2011 6th International Conference on

Conference_Location

Singapore

Print_ISBN

978-1-4244-9717-1

Type

conf

DOI

10.1109/ICCSE.2011.6028832

Filename

6028832