Modeling And Verification For Data-Centric Web Services
PROCEEDINGS OF 2013 IEEE 4TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND SERVICE SCIENCE (ICSESS)(2012)
摘要
We propose a model for a class of Web services which are powered by relational databases and respond to users by querying the underlying database as well as the state information of interaction. Our model can be viewed as an extension of WSDL specification where schemas of service operations specify not only input-output signatures but also data constraints, control-flow constraints, and state/output/action rules. The control-flow and more complex data-aware temporal properties about interactions between services and users are specified in Linear Temporal Logic (LTL) and its extension Linear Temporal First-Order Logic (LTL-FO). We have proved it is feasible to existing tools (e.g. SPIN, WAVE) to verify such properties.
更多查看译文
关键词
Web Service, Automatic Verification, Linear Temporal Logic
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络