RGPS过程层元模型正确性验证  

Correctness Verification of RGPS Process Level Meta-model

作　　者：袁开银[1] 郭瑞[2] 陆翔升[3] 吴尽昭[3] 

机构地区：[1]河南财经政法大学现代教育技术中心,郑州450002 [2]郑州轻工业学院计算机与通信工程学院,郑州450002 [3]中国科学院成都计算机应用研究所,成都610041

出　　处：《计算机工程》2012年第15期39-42,共4页Computer Engineering

基　　金：国家"863"计划基金资助项目"基于代数符号计算的新型软件形式化验证技术和支持工具"(2007AA01Z143)

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

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

分 类 号：TP393.07[自动化与计算机技术—计算机应用技术]