详细信息
文献类型:期刊文献
中文题名:RGPS过程层元模型正确性验证
英文题名:Correctness Verification of RGPS Process Level Meta-model
作者:袁开银[1];郭瑞[2];陆翔升[3];吴尽昭[3]
第一作者:袁开银
机构:[1]河南财经政法大学现代教育技术中心;[2]郑州轻工业学院计算机与通信工程学院;[3]中国科学院成都计算机应用研究所
第一机构:河南财经政法大学
年份:2012
卷号:38
期号:15
起止页码:39-42
中文期刊名:计算机工程
外文期刊名:Computer Engineering
收录:CSTPCD;;CSCD:【CSCD2011_2012】;
基金:国家"863"计划基金资助项目"基于代数符号计算的新型软件形式化验证技术和支持工具"(2007AA01Z143)
语种:中文
中文关键词:RGPS框架;Promela建模;Spin模型检测工具;过程层元模型;线性时序逻辑
外文关键词:Role Goal Process Service(RGPS) framework; Promela modeling; Spin model checking tool; process level meta-model; Linear Temporal Logic(LTL)
摘要:利用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.
参考文献:
正在载入数据...