Logic-based verification for Web services composition with TLA

Author

Wang, Hongbing ; Li, Li ; Wang, Chen ; Kang, Zuling ; Liu, Dongxi ; Wu, Jemma ; Bouguettaya, Athman

Author_Institution

Dept. of Comput. Sci. & Eng., Southeast Univ., Nanjing, China

fYear

2009

fDate

14-15 Jan. 2009

Firstpage

1

Lastpage

8

Abstract

Web services composition is an emerging paradigm for enabling application integration within and across organizational boundaries. Effectively verifying service composition to comply with the requirements is challenging. Verifying the composed service against certain properties is discussed in this paper. TLA (Temporal Logic of Actions) is introduced to enable effective verification. In particular, algorithms to transforming Web services from OWL-S to TLA are proposed. We then show that automatically verifying Web service behaviours can be achieved by using TLC (TLA model checking tool). A case study is given to illustrate the transformation and verification.

Keywords

Web services; formal verification; knowledge representation languages; temporal logic; OWLS; TLA model checking tool; Web services composition; logic-based verification; temporal logic of actions; Application software; Australia; Computer science; Feeds; Information science; Logic; Mathematical model; Semantic Web; Software engineering; Web services;

fLanguage

English

Publisher

ieee

Conference_Titel

Service-Oriented Computing and Applications (SOCA), 2009 IEEE International Conference on

Conference_Location

Taipei

Print_ISBN

978-1-4244-5300-9

Type

conf

DOI

10.1109/SOCA.2009.5410266

Filename

5410266