Web服务过程建模及其逻辑正确性验证

Modeling and logical correctness verification of Web service processes

为研究Web服务过程的逻辑正确性及其形式化验证方法,提出一种基于着色Petri网的Web服务过程模型,给出了逻辑正确性的形式化定义。为验证其正确性,提出通信可达树的概念,借助通信可达树的某些性质来验证服务的逻辑正确性,并给出了正确性判定定理。另外,为了简化组合服务逻辑正确性的验证过程,阐述了组合服务与其子服务之间的内在关系。最后,通过一个应用实例验证了方法的可用性。

To study the logical correctness of Web service processes and their formal verification method, a model based on Colored Petri Nets （CPNs） for Web service processes and the formal definition of the logical correctness were proposed. Based on the introduction of Communication Reachability Trees （CRTs）, an approach to correctness verification of Web service processes was developed. And a criteria theorem was also presented. Moreover, dependencies between the processes of a composite service and its components were discussed to simplify the verification. Particularly, a conclusion was presented that a composite service composed by well-structured services was logically correct if it could reach the final markings. Finally, an example was used to illustrate the applicability of this approach.