[1] Du Xutao, Xing Chunxiao, Zhou Lizhu, et al. Reachability analysis of web service compositions via NWA [J]. Journal of Southeast University (English Edition), 2008, 24 (3): 293-295. [doi:10.3969/j.issn.1003-7985.2008.03.010]

Copy

Reachability analysis of web service compositions via NWA()

Share：

Journal of Southeast University (English Edition)[ISSN:1003-7985/CN:32-1325/N]

Volumn:

24

Issue:

2008 3

Page:

293-295

Research Field:

Computer Science and Engineering

Publishing date:

2008-09-30

Info

Title:

Reachability analysis of web service compositions via NWA

Author(s):

Du Xutao¹;  Xing Chunxiao²;  3;  Zhou Lizhu¹

¹Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China
²Research Institute of Information Technology, Tsinghua University, Beijing 100084, China
³Tsinghua National Laboratory for Information Science and Technology, Tsinghua University, Beijing 100084, China

Keywords:

web service composition;  formalism;  nested word automata(NWA);  web service interface control flow automata(WCFA);  verification

PACS:

TP311

DOI:

10.3969/j.issn.1003-7985.2008.03.010

Abstract:

In order to improve the design and implementation quality of web service compositions, formal methods are used to model them and certain properties are verified.WCFA(web service interface control flow automata)is used to model web services, especially the control flow and possible interactions with other web services.A web service composition consists of a set of interacting WCFA.The global behavior of web service compositions is captured by NWA(nested word automata).A variation of the depth-first search algorithm is used to transform a set of WCFA into an NWA.State formulae and call stacks at each node of NWA are computed by a path-sensitive reachability analysis.Safety properties, call stack inspection properties and pre/post-conditions of service invocations are described by assertions.Then verification of these assertions is carried out by an automated SAT tool.

References:

[1] Beyer D, Chakrabarti A, Henzinger T A.Web service interfaces [C]//Proceedings of the 14th International World Wide Web Conference.New York:ACM, 2005:148-159.
[2] Du Xutao, Xing Chunxiao, Zhou Lizhu.Abstract reachability graph for verifying web service interfaces [C]//Proceedings of the 10th International Conference on Software Reuse.Beijing, China, 2008:262-265.
[3] Alur R, Madhusudan P.Adding nesting structure to words[C]//Proceedings of the 10th International Conference on Developments in Language Theory.Santa Barbara, 2006:1-13.
[4] Barrett C, Berezin S.CVC lite:a new implementation of the cooperating validity checker[C]//Proceedings of the 16th International Conference on Computer Aided Verification.Boston, 2004:515-518.
[5] Fu X, Bultan T, Su J.Analysis of interacting BPEL web services[C]//Proceedings of the 13th International World Wide Web Conference.New York:ACM, 2004:621-630.
[6] Foster H, Uchitel S, Magee J, et al.LTSA-WS:a tool for model-based verification of web service compositions and choreography [C]//Proceedings of the 28th International Conference on Software Engineering.Shanghai, China, 2006:771-774.
[7] Ouyang C, Verbeek H, van der Aalst W, et al.Wofbpel:a tool for automated analysis of BPEL processes[C]//Proceedings of the 3rd International Conference on Service-Oriented Computing(ICSOC).Amsterdam, Netherlands, 2005:484-489.

Memo

Memo:

Biographies: Du Xutao(1977—), male, graduate;Xing Chunxiao(corresponding author), male, doctor, professor, xingcx@tsinghua.edu.cn.
Foundation items: The National Key Technology R& D Program of China during the 11th Five-Year Plan Period(No.2006BAH02A12), the National High Technology Research and Development Program of China(863 Program)(No.2006AA010101).
Citation: Du Xutao, Xing Chunxiao, Zhou Lizhu.Reachability analysis of web service compositions via NWA[J].Journal of Southeast University(English Edition), 2008, 24(3):293-295.

Common functions