Web服务组合的性质检验与实现

【作者】 刘磊；

【导师】 周明天； 肖开奇；

【作者基本信息】 电子科技大学 ， 软件工程， 2009， 硕士

【摘要】 随着Web服务的出现和推广,基于Web服务的动态组合技术已成为近年来的研究热点。Web服务的业务流程执行语言(BPEL4WS)作为一种基于业务流程的服务组合方法,建模理论基础比较薄弱,组合正确性比较难以保证,所以Web服务组合的验证就显得十分重要,在服务被正式实施之前,必须通过验证来考查流程的正确性,无死锁性等问题。在这样的前提下,本文提出利用Pi演算和mu演算对BPEL4WS进行性质检验的方法,并开发出一个性质检验工具,对Web服务组合进行检验,包括安全性检验和可达性检验。该工具基本上实现了BPEL4WS的自动化检验,对检验时发现不满足性质的,则对错误处的片段进行标注,并把错误路径反馈到BPEL4WS源文件中。对用户来说,检验过程基本是一个透明的过程,用户不用深入了解具体的检验方法和知识,就可以直接利用本文开发的工具进行性质检验,并可针对检验后标识的地方进行改进。本文的结果说明对BPEL4WS文件的自动化性质检验和出错路径标识是可行的。更多还原

【Abstract】 Along with the prosperity and acceptance of the Web services, the technique of dynamic service composition based on Web Services has been regarded as one of the hot research topics. The Business Process Execution Language for Web services (BPEL4WS), as a service composition method based on business process, is weak in modeling and compositing. So the validity of the process and the property of non-deadlocks must be simulated and proved before the service composition is being implemented formally.According to the requirement mentioned above, using Pi-calculus and mu-calculus, a method for checking the property of BPEL4WS has been put forward in this thesis, as well as a tool for checking reachable and deadlocks.People could check BPEL4WS files roughly automatic on, when it finds error, it will tag error on BPEL4WS files.It is almost transparent, from modeling to checking, to user, the user who doesn’t understand the formal method thoroughly, can do the check using the tool and do the improvement at the tagged place. The simulation result shows that it is feasible to check the property of BPEL4WS and tag the error path automatically.更多还原