计算机工程2012，Vol.38Issue(15)：39-42,4.DOI:10.3969/j.issn.1000-3428.2012.15.011
RGPS过程层元模型正确性验证
Correctness Verification of RGPS Process Level Meta-model
摘要
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.关键词
RGPS框架/Promela建模/Spin模型检测工具/过程层元模型/线性时序逻辑Key words
Role Goal Process Service(RGPS) framework/ Promela modeling/ Spin model checking tool/ process level meta-model/ Linear Temporal Logic(LTL)分类
信息技术与安全科学引用本文复制引用
袁开银,郭瑞,陆翔升,吴尽昭..RGPS过程层元模型正确性验证[J].计算机工程,2012,38(15):39-42,4.基金项目
国家“863”计划基金资助项目“基于代数符号计算的新型软件形式化验证技术和支持工具”(2007AA01Z143) （2007AA01Z143）
