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.展开更多
This paper proposes a method of data-flow testing for Web services composition. Firstly, to facilitate data flow analysis and constraints collecting, the existing model representation of business process execution lan...This paper proposes a method of data-flow testing for Web services composition. Firstly, to facilitate data flow analysis and constraints collecting, the existing model representation of business process execution language （BPEL） is modified in company with the analysis of data dependency and an exact representation of dead path elimination （DPE） is proposed, which over-comes the difficulties brought to dataflow analysis. Then defining and using information based on data flow rules is collected by parsing BPEL and Web services description language （WSDL） documents and the def-use annotated control flow graph is created. Based on this model, data-flow anomalies which indicate potential errors can be discovered by traversing the paths of graph, and all-du-paths used in dynamic data flow testing for Web services composition are automatically generated, then testers can design the test cases according to the collected constraints for each path selected.展开更多
为了实现流程工业遗留系统的有效集成,提出了一种基于Web服务的流程工业遗留系统信息集成模型。首先,分析流程工业遗留系统的特点,确定遗留系统要公开的数据及功能,再利用Web Service Wrapper技术将其包装为Web服务;然后,企业可以根据...为了实现流程工业遗留系统的有效集成,提出了一种基于Web服务的流程工业遗留系统信息集成模型。首先,分析流程工业遗留系统的特点,确定遗留系统要公开的数据及功能,再利用Web Service Wrapper技术将其包装为Web服务;然后,企业可以根据自身的集成目标,动态地集成这些分布在不同区域的Web服务,该模型对遗留系统采用包装的方法,保证了遗留系统在集成平台中仍保持原先的安全稳定性;最后,通过在建立Mini-Plant的计算机信息集成平台上的实际应用,验证了该集成技术的有效性及实用性。展开更多
基金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.
基金the National Natural Science Foundation of China(60425206, 60503033)National Basic Research Program of China (973 Program, 2002CB312000)Opening Foundation of State Key Laboratory of Software Engineering in Wuhan University
文摘This paper proposes a method of data-flow testing for Web services composition. Firstly, to facilitate data flow analysis and constraints collecting, the existing model representation of business process execution language （BPEL） is modified in company with the analysis of data dependency and an exact representation of dead path elimination （DPE） is proposed, which over-comes the difficulties brought to dataflow analysis. Then defining and using information based on data flow rules is collected by parsing BPEL and Web services description language （WSDL） documents and the def-use annotated control flow graph is created. Based on this model, data-flow anomalies which indicate potential errors can be discovered by traversing the paths of graph, and all-du-paths used in dynamic data flow testing for Web services composition are automatically generated, then testers can design the test cases according to the collected constraints for each path selected.
文摘为了实现流程工业遗留系统的有效集成,提出了一种基于Web服务的流程工业遗留系统信息集成模型。首先,分析流程工业遗留系统的特点,确定遗留系统要公开的数据及功能,再利用Web Service Wrapper技术将其包装为Web服务;然后,企业可以根据自身的集成目标,动态地集成这些分布在不同区域的Web服务,该模型对遗留系统采用包装的方法,保证了遗留系统在集成平台中仍保持原先的安全稳定性;最后,通过在建立Mini-Plant的计算机信息集成平台上的实际应用,验证了该集成技术的有效性及实用性。
