组合Web服务的建模与验证

项目名称： 组合Web服务的建模与验证

项目编号： No.60873018

项目类型： 面上项目

立项/批准年度： 2009

项目学科： 武器工业

项目作者： 段振华

作者单位： 西安电子科技大学

项目金额： 36万元

中文摘要： 以投影时序逻辑的可执行子集Framed Tempura 为基础，定义组合Web 服务建模语言WS-Tempura 的语句结构和通信机制，研究该语言的操作语义，并开发该语言的解释器。研究该语言的正则形及正则图，研究该语言的可判定性，判定算法及算法复杂度。研究BPEL 流程到WS-Tempura 程序的转换规则，并开发自动转换工具，以实现BPEL 流程模型的自动提取。研究基于WS-Tempura 程序执行的仿真和错误诊断技术；基于执行生成的正则图，研究该图的性质以及相关的程序分析技术。以WS-Tempura 建模语言描述组合Web 服务的行为，以PPTL 描述组合Web 服务的性质，研究基于模型检测工具SPIN 的验证方法；同时，在由WS-Tempura 和PPTL 组成的统一时序逻辑框架下，研究基于SAT 的模型、性质一体化的组合Web 服务验证方法。

中文关键词： 组合Web 服务；模型检测；投影时序逻辑；仿真；验证

英文摘要： Based on the executable subset of projection temporal logic (PTL), Framed Tempura, we defined the statement structure and communication mechanism of WS-Tempura, a modeling language of web service composition, researched its operational semantics and developed an interpreter for it. Then we studied the normal form, normal form graph, decidability and decision algorithm and its complexity of WS-tempura. To implement the automatic extraction of BPEL's flow model, we made a research on the transformational rule from BPEL's flow to WS-Tempura program and developed an automatic tool for the transformation. Further, we discussed not only the simulation and error diagnostic techniques but also the normal form graph, properties of the normal form and relevant procedure analysis techniques based on the run of WS-Tempura program. Using the modeling language WS-Tempura to describe behaviors and PPTL to specify properties of web service composition, we studied the verification techniques based on model checker SPIN. We also researched the integrative verification of model and property based on SAT in the frame of unified temporal logic composed of WS-Tempura and PPTL.

英文关键词： web service composition;model checking;projection temporal logic(PTL);simulation;verification