CAJ | 학술논문

服务编制解决的是组织之间的业务集成问题,面临的是一个广泛分布、动态、自治、异构的网络环境,保障组合服务的正确执行以及相关特性的验证问题显得尤为重要.形式化方法是一种有效的解决方法,服务编制需要建立在严格的形式化模型的基础上,可以通过具有明确的、形式化语义的形式化模型研制验证工具来完成组合服务正确性的验证.本文基于并发事务逻辑(CTR:Concurrent TRansaction Logic)对服务编制的元素进行了描述和建模,给出了从WS-BPEL到并发事务逻辑的转换规则,讨论了服务编制在CTR中的验证问题以及WS-BPEL和CTR的表达能力,最后给出了一个实际的服务编制在CTR中建模的例子,验证了服务编制的CTR模型的有效性.
복무편제해결적시조직지간적업무집성문제,면림적시일개엄범분포、동태、자치、이구적망락배경,보장조합복무적정학집행이급상관특성적험증문제현득우위중요.형식화방법시일충유효적해결방법,복무편제수요건립재엄격적형식화모형적기출상,가이통과구유명학적、형식화어의적형식화모형연제험증공구래완성조합복무정학성적험증.본문기우병발사무라집(CTR:Concurrent TRansaction Logic)대복무편제적원소진행료묘술화건모,급출료종WS-BPEL도병발사무라집적전환규칙,토론료복무편제재CTR중적험증문제이급WS-BPEL화CTR적표체능력,최후급출료일개실제적복무편제재CTR중건모적례자,험증료복무편제적CTR모형적유효성.
Web services solve the problem of inter-organization business integration and are under a distributed, dynamic, au-tonomic and heterogeneous environment.The correctness and verification of web service orchestration is important.Formalization is a valid method. This paper gives the specification of web service orchestration based on concurrent transaction logic. The translation rules from WS-BPEL to concurrent transaction logic are given. The verification problem of web service orchestration based on concurrent transaction logic is discussed.Finally,an actual web service orchestration model based on concurrent transaction logic is illustrated.