|Table of Contents|

[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()
使用NWA对组合web服务进行可达性分析
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
使用NWA对组合web服务进行可达性分析
Author(s):
Du Xutao1;  Xing Chunxiao2;  3;  Zhou Lizhu1
1Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China
2Research Institute of Information Technology, Tsinghua University, Beijing 100084, China
3Tsinghua National Laboratory for Information Science and Technology, Tsinghua University, Beijing 100084, China
杜旭涛1;  邢春晓2;  3;  周立柱1
1清华大学计算机科学与技术系, 北京 100084; 2清华大学信息技术研究院, 北京 100084; 3清华大学清华信息科学与技术国家实验室, 北京 100084
Keywords:
web service composition;  formalism;  nested word automata(NWA);  web service interface control flow automata(WCFA);  verification
组合web服务;  形式化方法;  嵌套字自动机;  web服务接口控制流自动机;  验证
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.
为了提高组合web服务的设计和实现质量, 使用形式化方法对其进行建模并对其关键性质进行验证.使用web服务接口控制流自动机(WCFA)对web服务进行建模, 主要描述其控制流及与其他web服务的交互关系.组合web服务由一组交互的WCFA组成.使用嵌套字自动机(NWA)对组合web服务的整体行为进行建模.将一组WCFA转换为嵌套字自动机(NWA)的算法是深度优先搜索算法的变种, 算法中使用路径相关的可达性分析计算NWA的每个节点的状态公式和调用栈.安全性相关性质、调用栈相关性质及服务调用的前置和后置条件都可以用断言来描述, 然后使用一个自动的可满足性(SAT)求解工具对这些断言进行验证.

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.
Last Update: 2008-09-20