Reachability analysis of web service compositions via NWA

作     者：杜旭涛 邢春晓 周立柱 Du Xutao;Xing Chunxiao;Zhou Lizhu

作者机构：清华大学计算机科学与技术系北京100084 清华大学信息技术研究院 

基　　金：The National Key Technology R&D Program of Chinaduring the 11th Five-Year Plan Period(No.2006BAH02A12) the National High Technology Research and Development Program of China(863 Program)(No.2006AA010101) 

出 版 物：《Journal of Southeast University(English Edition)》 (东南大学学报（英文版）)

年 卷 期：2008年第24卷第3期

页      码：293-295页

摘      要：In order to improve the design and implementation quality of web service compositions,formal methods are used to model them and certain properties are *** （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 *** 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 *** formulae and call stacks at each node of NWA are computed by a path-sensitive reachability *** properties,call stack inspection properties and pre/post-conditions of service invocations are described by *** verification of these assertions is carried out by an automated SAT tool.

主 题 词：web service composition formalism nested word automata (NWA) web service interface control flow automata (WCFA) verification 

学科分类：0810[工学-土木类] 08[工学] 0805[工学-能源动力学] 0835[0835] 0812[工学-测绘类] 081202[081202] 

核心收录：

D　O　I：10.3969/j.issn.1003-7985.2008.03.010

馆 藏 号：203101916...