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

• 作者: 吴尽昭 袁开银 郭瑞 陆翔升
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: RGPS框架 Promela建模 Spin模型检测工具 过程层元模型 线性时序逻辑
• 年，卷（期）: 2012,（15）
• 所属期刊栏目: 软件技术与数据库
• 页码范围: 39-42
• 分类号: TP393.07
• 字数: 3079字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2012.15.011

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	吴尽昭	中国科学院成都计算机应用研究所	23	81	4.0	8.0
2	郭瑞	郑州轻工业学院计算机与通信工程学院	19	75	6.0	7.0
3	袁开银	河南财经政法大学现代教育技术中心	11	28	3.0	5.0
4	陆翔升	中国科学院成都计算机应用研究所	1	1	1.0	1.0