WS-Addressing用端点引用(EndpointReference,EPR)来进行Web服务寻址,EPR是动态生成的服务端点描述,它不能直接存储在统一描述、发现和集成(universal description discovery and integration,UDDI)的静态数据结构中。为实现UDDI和WS-Ad...WS-Addressing用端点引用(EndpointReference,EPR)来进行Web服务寻址,EPR是动态生成的服务端点描述,它不能直接存储在统一描述、发现和集成(universal description discovery and integration,UDDI)的静态数据结构中。为实现UDDI和WS-Addressing共存的Web服务模型,提供了在UDDI中支持WS-Addressing的方法,并通过购物车的实现来说明应用程序应如何支持WS-Addressing。展开更多
Model checking techniques have been widely used in verifying web service compositions to ensure the trustworthi- ness. However, little research has focused on testing web services. Based on the research of model check...Model checking techniques have been widely used in verifying web service compositions to ensure the trustworthi- ness. However, little research has focused on testing web services. Based on the research of model checking techniques~ we propose a model checking based approach for testing web service composition which is described by using the web services choreography description language （WS-CDL）. According to worldwide web consortium （W3C） candidate recommendation, the WS-CDL specification provides a language for characterizing interactions between distinct web services using XML. Since the behaviors of web service composition are asynchronous, distributed, low-coupled and platform independent, we employ the guarded automata （GA） model for specifying the composition described in WS-CDL and using the simple promela interpreter （SPIN） model checker for detecting the collaborations of web services. Test cases can be transformed from counterexamples generated by SPIN using adequacy criteria. In this paper we apply the transition coverage criterion for generating counterex- amples. To illustrate our approach, we set ＂E-commerce service system＂ as an example for demonstrating how test cases can be generated using SPIN for compositions specified in WS-CDL.展开更多
Web service （WS） is an emerging software technology, especially acting an important role in cloud computing. The WS choreography description language （WS-CDL） is the standard for modeling the observable behavior o...Web service （WS） is an emerging software technology, especially acting an important role in cloud computing. The WS choreography description language （WS-CDL） is the standard for modeling the observable behavior of WS composition across multiple participants from a global point of view. However, it lacks of a formal semantics and could easily lead to misunderstanding and different implementations. In this paper, the WS-CDL based specifications are formally extracted in a communicating sequential process supporting a formal approach to checking WS models. In addition, formalisms and model checking are explicitly illustrated through a simple but non-trivial example with the help of model checker process analysis toolkit （PAT）.展开更多
文摘WS-Addressing用端点引用(EndpointReference,EPR)来进行Web服务寻址,EPR是动态生成的服务端点描述,它不能直接存储在统一描述、发现和集成(universal description discovery and integration,UDDI)的静态数据结构中。为实现UDDI和WS-Addressing共存的Web服务模型,提供了在UDDI中支持WS-Addressing的方法,并通过购物车的实现来说明应用程序应如何支持WS-Addressing。
基金Project supported by the Open Foundation of State Key Laboratory of Software Engineering(Grant No.SKLSE20080712)the National Natural Science Foundation of China(Grant No.60970007)+2 种基金the National Basic Research Program of China(Grant No.2007CB310800)the Shanghai Leading Academic Discipline Project(Grant No.J50103)the Science and Technology Commission of Shanghai Municipality(Grant No.09DZ2272600)
文摘Model checking techniques have been widely used in verifying web service compositions to ensure the trustworthi- ness. However, little research has focused on testing web services. Based on the research of model checking techniques~ we propose a model checking based approach for testing web service composition which is described by using the web services choreography description language （WS-CDL）. According to worldwide web consortium （W3C） candidate recommendation, the WS-CDL specification provides a language for characterizing interactions between distinct web services using XML. Since the behaviors of web service composition are asynchronous, distributed, low-coupled and platform independent, we employ the guarded automata （GA） model for specifying the composition described in WS-CDL and using the simple promela interpreter （SPIN） model checker for detecting the collaborations of web services. Test cases can be transformed from counterexamples generated by SPIN using adequacy criteria. In this paper we apply the transition coverage criterion for generating counterex- amples. To illustrate our approach, we set ＂E-commerce service system＂ as an example for demonstrating how test cases can be generated using SPIN for compositions specified in WS-CDL.
基金supported by the Shanghai Leading Academic Discipline Project (Grant No.J50103)
文摘Web service （WS） is an emerging software technology, especially acting an important role in cloud computing. The WS choreography description language （WS-CDL） is the standard for modeling the observable behavior of WS composition across multiple participants from a global point of view. However, it lacks of a formal semantics and could easily lead to misunderstanding and different implementations. In this paper, the WS-CDL based specifications are formally extracted in a communicating sequential process supporting a formal approach to checking WS models. In addition, formalisms and model checking are explicitly illustrated through a simple but non-trivial example with the help of model checker process analysis toolkit （PAT）.
