Reachability analysis of Web service interfaces

Author

Du, Xutao ; Xing, Chunxiao ; Zhou, Lizhu

Author_Institution

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

fYear

2008

fDate

13-15 July 2008

Firstpage

40

Lastpage

45

Abstract

We use WCFA (Web Service Interface Control Flow Automata) to model web service interfaces. Global behaviors of web service compositions are captured by abstract reachability graph(ARG). A polynomial time algorithm for the construction of ARG is presented. The algorithm uses a reachability analysis to verify both safety and call stack inspection properties. Both kinds of properties are expressed by assertions at control points of ARG. Each control point is equipped with a state formula and a call stack. Verification is done by a SAT solver which checks whether the assertions are logical consequences of the state formulas(or the call stacks).

Keywords

Automata; Automatic control; Collaborative software; Information science; Information technology; Inspection; Laboratories; Reachability analysis; Safety; Web services;

fLanguage

English

Publisher

ieee

Conference_Titel

Information Reuse and Integration, 2008. IRI 2008. IEEE International Conference on

Conference_Location

Las Vegas, NV, USA

Print_ISBN

978-1-4244-2659-1

Electronic_ISBN

978-1-4244-2660-7

Type

conf

DOI

10.1109/IRI.2008.4583002

Filename

4583002