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

摘要：

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

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

所属期刊栏目：38

分类号：TP393.07(计算技术、计算机技术)

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

在线出版日期：2012-11-16（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：39-42