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

Model checking analysis of observational transition system with SMV

作　　者：何涛[1] 缪淮扣[1] 

机构地区：[1]上海大学计算机工程与科学学院,上海200072

出　　处：《计算机工程与设计》2008年第18期4750-4752,4761,共4页Computer Engineering and Design

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

摘　　要：模型检验技术是开发高可信系统的重要途径。提出了一种基于定理证明的模型验证方法,并实现了工具验证。它以代数规约语言CafeOBJ描述系统的无限状态并把它转换成有限状态的SMV规约。通过观察迁移系统,证明产生的SMV规约的反例即CafeOBJ规约的反例,来找出开发早期阶段的系统的潜在错误,从而避免时间、金钱的耗费及重复性的劳动。Model checking is an important way in developing high confidence systems. A model checking method based on theorem proving is proposed, which describes the infinite system state by CafeOBJ and transfers a CafeOBJ specification to a finite SMV specification, and its tool is implemented. By observing transition system shows that a counter example of a corresponding SMV specification is also a counter example of a CafeOBJ specification. It find errors lurked in systems at earlier stages of their development processes to avoid spending much money and time to correct errors later.

关 键 词：模型检测 模型验证 SMV CafeOBJ 模型检查工具 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]