TY - GEN
T1 - Verifying transactional requirements of web service compositions using temporal logic templates
AU - Bourne, Scott
AU - Szabo, Claudia
AU - Sheng, Quan Z.
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84887456785&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-41230-1_21
DO - 10.1007/978-3-642-41230-1_21
M3 - Conference proceeding contribution
AN - SCOPUS:84887456785
SN - 9783642412295
T3 - Lecture Notes in Computer Science
SP - 243
EP - 256
BT - Web Information Systems Engineering - WISE 2013
A2 - Lin, Xuemin
A2 - Manolopoulos, Yannis
A2 - Srivastava, Divesh
A2 - Huang, Guangyan
PB - Springer, Springer Nature
CY - Heidelberg, Germany
T2 - 14th International Conference on Web Information Systems Engineering, WISE 2013
Y2 - 13 October 2013 through 15 October 2013
ER -