组合Web服务的建模与验证

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