Title :
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
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;
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
DOI :
10.1109/IRI.2008.4583002
