题目：基于工作流网的WS-BPEL正确性验证方法研究与实现

WS-BPEL是一种主流的Web服务组合语言，而工作流网在WS-BPEL的形式化验证中得到广泛应用，但当前WS-BPEL的工作流网模型大多只针对WS-BPEL流程的控制流建模，缺少数据信息，对WS-BPEL流程中存在的数据访问异常不能进行检测。针对上述问题，论文对工作流网进行了扩展，提出了数据工作流网的概念。数据工作流网既保持了工作流网对WS-BPEL流程控制流建模的完备性，又可以实现对流程中的数据流建模。本论文首先分析了WS-BPEL流程中可能存在的问题，在给出数据工作流网的形式化定义后，给出流程中存在的问题在数据工作流网中所反映的特性。随后，论文提出了WS-BPEL各元素的数据工作流网模型，给出WS-BPEL流程至数据工作流网转换的方法，并实现了WS-BPEL流程的数据工作流网建模工具。WS-BPEL流程的数据工作流网模型使用目前应用广泛的PNML描述，为了能对数据工作流网中的数据信息进行描述，本文对PNML进行扩展，定义了数据工作流网的PNTD。论文进一步研究开发了数据工作流网分析工具，该工具导入PNML描述的数据工作流网，并基于可达图对网的各项特性进行分析。鉴于当前某些被广泛应用的可达图算法存在效率较低的问题，本论文对可达图算法加以改进，避免了相同标记节点重复计算的问题，提高了可达图的计算效率，并提出了基于可达图对数据工作流网的终态可达性、死锁、活锁和数据访问异常进行检测的算法。论文提出的数据工作流网的概念，使得基于工作流网可以实现对WS-BPEL流程的数据流建模，并可检测流程中存在的数据访问异常；数据工作流网分析工具对PNML的支持，使得任何使用PNML描述的P/T系统，均可使用此工具进行死锁、活锁和终态可达性分析。论文的研究成果为Web组合服务应用的建立，提供了有效的支持。