论文部分内容阅读
BPEL（业务流程执行语言）作为一种Web服务组装协议，是使用XML编写的用于描述Web服务静态组装结构的形式规约语言。为了使BPEL所描述的Web服务组装能够满足设计人员的设计初衷。人们尝试使用各种形式化方法对BPEL进行建模，在此基础上分析和验证Web服务组装的性质，从而保证用BPEL描述的Web服务组装是正确的。同步网是一种描述工作流的形式化模型，徐春香等基于这种模型给出了BPEL逻辑层活动的形式化建模方法。
本文在同步网形式化建模的基础上，提出了基于BPEL的Web服务组装所具有的六种常用的性质：为了验证这些性质，在原有P/T_系统可达图的基础上，提出了同步网可达图的概念；并针对同步网模型的特征，给出了同步网可达图的构造方法。基于可达性的验证，本文给出了上述六种Web服务组装性质的验证方法。
为了检查上述理论模型和验证方法的有效性，本文开发了一个原型工具，实现了对BPEL的同步网建模过程和上述六种性质的验证算法；该软件集成了形式化模型检测工具SPIN，可以对用户使用LTL描述的Web服务组装性质进行验证。从而，实现了一种针对BPEL逻辑层的自动化建模、常用性质分析和LTL性质验证的工具——基于同步网的BPEL辅助分析工具（BPELAnalyzeTool）。通过使用该工具对BPEL实例进行分析，得到的分析结果证明了该T具的有效性。