Int. J. of Wireless and Mobile Computing   »   2014 Vol.7, No.3

 

 

Title: Verification for commitment-based web service protocols

 

Authors: Zhi Fang; Lejian Liao; Ruoyu Chen

 

Addresses:
Beijing Engineering Research Centre of High Volume Language Information Processing & Cloud Computing Applications, Beijing Laboratory of Intelligent Information Technology, School of Computer Science, Beijing Institute of Technology, Beijing 100081, China
Beijing Engineering Research Centre of High Volume Language Information Processing & Cloud Computing Applications, Beijing Laboratory of Intelligent Information Technology, School of Computer Science, Beijing Institute of Technology, Beijing 100081, China
Beijing Engineering Research Centre of High Volume Language Information Processing & Cloud Computing Applications, Beijing Laboratory of Intelligent Information Technology, School of Computer Science, Beijing Institute of Technology, Beijing 100081, China

 

Abstract: We propose a model for a class of web services which are powered by relational databases and annotated by social commitment. 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, state/output/effect rules. The data-aware temporal properties about interactions between services and users are specified in Linear Temporal First-Order Logic with Social Commitment (LTL-FOSC). We have proved it is possible to use existing tools (e.g. WAVE) originally designed for verification of web applications to verify such properties.

 

Keywords: commitment-based web services; web service protocols; automatic verification; linear temporal logic; relational databases; social commitment.

 

DOI: 10.1504/IJWMC.2014.062006

 

Int. J. of Wireless and Mobile Computing, 2014 Vol.7, No.3, pp.217 - 223

 

Submission date: 19 May 2013
Date of acceptance: 21 Jul 2013
Available online: 29 May 2014

 

 

Editors Full text accessAccess for SubscribersPurchase this articleComment on this article