SMV的观察迁移系统的模型检测分析

作     者：何涛 缪淮扣 HE Tao;MIAO Huai-kou

作者机构：上海大学计算机工程与科学学院上海200072 

基　　金：国家自然科学基金项目(60673115) 国家863高技术研究发展计划基金项目(2007AA01Z144) 国家973重点基础研究发展计划基金项目(2007CB310800) 上海市教委科研基金项目(07ZZ06) 上海市重点学科建设基金项目(J50103) 

出 版 物：《计算机工程与设计》 (Computer Engineering and Design)

年 卷 期：2008年第29卷第18期

页      码：4750-4752,4761页

摘      要：模型检验技术是开发高可信系统的重要途径。提出了一种基于定理证明的模型验证方法,并实现了工具验证。它以代数规约语言CafeOBJ描述系统的无限状态并把它转换成有限状态的SMV规约。通过观察迁移系统,证明产生的SMV规约的反例即CafeOBJ规约的反例,来找出开发早期阶段的系统的潜在错误,从而避免时间、金钱的耗费及重复性的劳动。

主 题 词：模型检测 模型验证 SMV CafeOBJ 模型检查工具 

学科分类：08[工学] 081202[081202] 0812[工学-测绘类] 

D　O　I：10.16208/j.issn1000-7024.2008.18.020

馆 藏 号：203301938...