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

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