In order to formally reason and verify web services composition described by web services choreography specification WS-CDL,a typed formal model named typed Abstract WS-CDL（web services choreography description langu...In order to formally reason and verify web services composition described by web services choreography specification WS-CDL,a typed formal model named typed Abstract WS-CDL（web services choreography description language）for WS-CDL specifications is proposed.In typed Abstract WS-CDL,the syntax of type and session,typing rules and operational semantics are formalized;the collaborations of web services are formally described by sessions;the operational semantics of a session can help to formally reason the execution of the choreography;the typing rules can help to formally check the data type consistency of exchanged information between web services and capture run-time errors due to type mismatches.Particularly,the concepts of type assumption set extension and type assumption set compatibility are proposed,and the merging algorithm of type assumption sets is defined so as to eliminate type assumption conflict.Based on the formal model,typed mapping rules for mapping web services choreography to orchestration is also defined.With the typed mapping rules,orchestration stubs and their type assumption sets can be generated from a given choreography; thus, web services composition can be verified at choreography and orchestration levels,respectively.The model is proved to have properties of type safety,and how the model can help to reason and verify web services composition is illustrated through a case study.展开更多
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）.展开更多
Recent advancements in cloud computing(CC)technologies signified that several distinct web services are presently developed and exist at the cloud data centre.Currently,web service composition gains maximum attention ...Recent advancements in cloud computing(CC)technologies signified that several distinct web services are presently developed and exist at the cloud data centre.Currently,web service composition gains maximum attention among researchers due to its significance in real-time applications.Quality of Service(QoS)aware service composition concerned regarding the election of candidate services with the maximization of the whole QoS.But these models have failed to handle the uncertainties of QoS.The resulting QoS of composite service identified by the clients become unstable and subject to risks of failing composition by end-users.On the other hand,trip planning is an essential technique in supporting digital map services.It aims to determine a set of location based services(LBS)which cover all client intended activities quantified in the query.But the available web service composition solutions do not consider the complicated spatio-temporal features.For resolving this issue,this study develops a new hybridization of the firefly optimization algorithm with fuzzy logic based web service composition model(F3L-WSCM)in a cloud environment for location awareness.The presented F3L-WSCM model involves a discovery module which enables the client to provide a query related to trip planning such as flight booking,hotels,car rentals,etc.At the next stage,the firefly algorithm is applied to generate composition plans to minimize the number of composition plans.Followed by,the fuzzy subtractive clustering(FSC)will select the best composition plan from the available composite plans.Besides,the presented F3L-WSCM model involves four input QoS parameters namely service cost,service availability,service response time,and user rating.An extensive experimental analysis takes place on CloudSim tool and exhibit the superior performance of the presented F3L-WSCM model in terms of accuracy,execution time,and efficiency.展开更多
Web-services are highly distributed programs, and concurrent software is notoriously error-prone. Model checking is a powerful technique to find bugs in concurrent systems. However, the existing model checkers have no...Web-services are highly distributed programs, and concurrent software is notoriously error-prone. Model checking is a powerful technique to find bugs in concurrent systems. However, the existing model checkers have no enough ability to support for the programming languages and communication mechanisms used for Web services. We propose to use Kripke structures as means of modeling Web service. This paper presents an automated way to extract formal models from programs implementing Web services using predicate abstraction for abstract model checking. The abstract models are checked by means of a model checker that implements automatic abstraction refinement. These results enable the verification of the applications that implement Web services.展开更多
基金The National Natural Science Foundation of China(No.60403027,60773191,70771043)the National High Technology Research and Development Program of China(863 Program)(No.2007AA01Z403)
文摘In order to formally reason and verify web services composition described by web services choreography specification WS-CDL,a typed formal model named typed Abstract WS-CDL（web services choreography description language）for WS-CDL specifications is proposed.In typed Abstract WS-CDL,the syntax of type and session,typing rules and operational semantics are formalized;the collaborations of web services are formally described by sessions;the operational semantics of a session can help to formally reason the execution of the choreography;the typing rules can help to formally check the data type consistency of exchanged information between web services and capture run-time errors due to type mismatches.Particularly,the concepts of type assumption set extension and type assumption set compatibility are proposed,and the merging algorithm of type assumption sets is defined so as to eliminate type assumption conflict.Based on the formal model,typed mapping rules for mapping web services choreography to orchestration is also defined.With the typed mapping rules,orchestration stubs and their type assumption sets can be generated from a given choreography; thus, web services composition can be verified at choreography and orchestration levels,respectively.The model is proved to have properties of type safety,and how the model can help to reason and verify web services composition is illustrated through a case study.
基金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）.
文摘Recent advancements in cloud computing(CC)technologies signified that several distinct web services are presently developed and exist at the cloud data centre.Currently,web service composition gains maximum attention among researchers due to its significance in real-time applications.Quality of Service(QoS)aware service composition concerned regarding the election of candidate services with the maximization of the whole QoS.But these models have failed to handle the uncertainties of QoS.The resulting QoS of composite service identified by the clients become unstable and subject to risks of failing composition by end-users.On the other hand,trip planning is an essential technique in supporting digital map services.It aims to determine a set of location based services(LBS)which cover all client intended activities quantified in the query.But the available web service composition solutions do not consider the complicated spatio-temporal features.For resolving this issue,this study develops a new hybridization of the firefly optimization algorithm with fuzzy logic based web service composition model(F3L-WSCM)in a cloud environment for location awareness.The presented F3L-WSCM model involves a discovery module which enables the client to provide a query related to trip planning such as flight booking,hotels,car rentals,etc.At the next stage,the firefly algorithm is applied to generate composition plans to minimize the number of composition plans.Followed by,the fuzzy subtractive clustering(FSC)will select the best composition plan from the available composite plans.Besides,the presented F3L-WSCM model involves four input QoS parameters namely service cost,service availability,service response time,and user rating.An extensive experimental analysis takes place on CloudSim tool and exhibit the superior performance of the presented F3L-WSCM model in terms of accuracy,execution time,and efficiency.
基金the National Natural Science Foundation of China (60663005, 60563005)the Natural Science Foundation of Guangxi Province (0542036, 0728093, 0728089)
文摘Web-services are highly distributed programs, and concurrent software is notoriously error-prone. Model checking is a powerful technique to find bugs in concurrent systems. However, the existing model checkers have no enough ability to support for the programming languages and communication mechanisms used for Web services. We propose to use Kripke structures as means of modeling Web service. This paper presents an automated way to extract formal models from programs implementing Web services using predicate abstraction for abstract model checking. The abstract models are checked by means of a model checker that implements automatic abstraction refinement. These results enable the verification of the applications that implement Web services.
