Please use this identifier to cite or link to this item:
https://hdl.handle.net/2440/82802
Citations | ||
Scopus | Web of Science® | Altmetric |
---|---|---|
?
|
?
|
Type: | Conference paper |
Title: | Verifying transactional requirements of web service compositions using temporal logic templates |
Author: | Bourne, S. Szabo, C. Sheng, Q. |
Citation: | Web Information Systems Engineering, WISE 2013, 14th International Conference, Nanjing, China, 13-15 October 2013, Proceedings, part 1/ Xuemin Lin, Yannis Manolopoulos, Divesh Srivastava, Guangyan Huang (eds.): pp.243-256 |
Publisher: | Springer |
Publisher Place: | Germany |
Issue Date: | 2013 |
Series/Report no.: | Lecture Notes in Computer Science |
ISBN: | 9783642412295 |
ISSN: | 0302-9743 1611-3349 |
Conference Name: | International Conference on Web Information Systems Engineering (14th : 2013 : Nanjing, China) |
Editor: | Lin, X. Manolopoulos, Y. Srivastava, D. Huang, G. |
Statement of Responsibility: | Scott Bourne, Claudia Szabo, and Quan Z. Sheng |
Abstract: | Ensuring reliability in Web service compositions is of crucial interest as services are composed and executed in long-running, distributed mediums that cannot guarantee reliable communications. Towards this, transactional behavior has been proposed to handle and undo the effects of faults of individual components. Despite significant research interest, challenges remain in providing an easy-to-use, formal approach to verify transactional behavior of Web service compositions before costly development. In this paper, we propose the use of temporal logic templates to specify component-level and composition-level transactional requirements over a Web service composition. These templates are specified using a simple format, configured according to scope and cardinality, and automatically translated into temporal logic. To verify design conformance to a set of implemented templates, we employ model checking. We propose an algorithm to address state space explosion by reducing the models into semantically equivalent Kripke structures. Our approach facilitates the implementation of expressive transactional behavior onto existing complex services, as demonstrated in our experimental study. |
Description: | Lecture notes in computer science, 2013, vol. 8180 LNCS (Part 1) |
Rights: | © Springer-Verlag Berlin Heidelberg 2013 |
DOI: | 10.1007/978-3-642-41230-1_21 |
Published version: | http://dx.doi.org/10.1007/978-3-642-41230-1_21 |
Appears in Collections: | Aurora harvest Computer Science publications |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
RA_hdl_82802.pdf | Restricted Access | 404.4 kB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.