GIS服务链的形式化建模与正确性验证

Study on the Formal Model and Correctnessverifying of GIS Service Chain

空间信息服务链作为空间信息服务一项重要的增值功能,为空间信息服务的重用与自动化组合提供了应用基础。对于空间信息服务链而言,保证其运行结果满足需求是实现增值服务的一个重要条件,因此,需要对其进行正确性验证。本文引入了Pi演算的等价理论,通过建立一个实际的空间信息服务链模型,用Pi演算对其进行形式化建模,并利用形式化工具对空间信息服务链是否满足用户需求(即正确性)进行了验证。

As an important value - added function for GIS service, GIS service chain provides the application foundation for reusing and automation composition GIS services. An important issue for realizing the value - added service is ensuring the operation results of GIS service chain meet the user needs, so it needs to verify the correctness of GIS service chain. This paper introduces the equivalence theory of Pi - calculus. A practical GIS service chain formal model is established using Pi - calculus. The validity of GIS service chain model and whether it meets the need are verified using the formal tools.