摘要： 利用Web服务本体描述语言对RGPS过程层元模型进行描述，建立Promela模型。基于线性时序逻辑，以及Spin检测工具的偏序规约和on-the-fly等优化技术对Promela模型进行正确性验证，设计并实现RGPS过程层元模型正确性验证平台。通过城市交通系统实例证明该验证方法的正确性和有效性。

关键词: RGPS框架, Promela建模, Spin模型检测工具, 过程层元模型, 线性时序逻辑

Abstract: This paper establishes the Promela model of the Web Ontology Language for Service(OWL-S) process model for Role Goal Process Service(RGPS) process level meta-model, uses Linear Temporal Logic(LTL) to describe the properties of models, and uses the partial order reduction and on-the-fly optimization techniques of model checking tools Spin to verify the properties. It designs and implements RGPS process level meta-model correctness verification platform. The effectiveness of this verification framework is demonstrated by a case study in urban transportation system.

Key words: Role Goal Process Service(RGPS) framework, Promela modeling, Spin model checking tool, process level meta-model, Linear Temporal Logic(LTL)

中图分类号: 

• TP393.07