在Web服务业务流程建模和实现过程中,Web服务编排从全局角度描述了Web服务参与者之间的协作和交互过程;Web服务编制描述了单个Web服务参与者与其他参与者的交互,两者的结合能有效提高服务流程建模和实现的效率以及准确性,但必须解决Web...在Web服务业务流程建模和实现过程中,Web服务编排从全局角度描述了Web服务参与者之间的协作和交互过程;Web服务编制描述了单个Web服务参与者与其他参与者的交互,两者的结合能有效提高服务流程建模和实现的效率以及准确性,但必须解决Web服务编排和服务编制的一致性验证问题。提出了一种基于CSP(communication sequence process)的Web服务编排语言WS-CDL(Web service choreography description lan-guage)和Web服务编制规范WS-BPEL(Web service business process execution language)间的一致性验证方法。该方法将WS-CDL和WS-BPEL均转换为CSP语言;然后基于CSP的模型检测工具PAT(process analysis toolkit)进行两者的一致性检查;最后通过一个完备的案例对该方法进行了验证,结果表明了该方法的有效性。展开更多
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服务业务流程建模和实现过程中,Web服务编排从全局角度描述了Web服务参与者之间的协作和交互过程;Web服务编制描述了单个Web服务参与者与其他参与者的交互,两者的结合能有效提高服务流程建模和实现的效率以及准确性,但必须解决Web服务编排和服务编制的一致性验证问题。提出了一种基于CSP(communication sequence process)的Web服务编排语言WS-CDL(Web service choreography description lan-guage)和Web服务编制规范WS-BPEL(Web service business process execution language)间的一致性验证方法。该方法将WS-CDL和WS-BPEL均转换为CSP语言;然后基于CSP的模型检测工具PAT(process analysis toolkit)进行两者的一致性检查;最后通过一个完备的案例对该方法进行了验证,结果表明了该方法的有效性。
基金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.
