| SMV的观察迁移系统的模型检测分析 |
| |
| 引用本文： | 何涛,缪淮扣.SMV的观察迁移系统的模型检测分析[J].计算机工程与设计,2008,29(18). |
| |
| 作者姓名： | 何涛 缪淮扣 |
| |
| 作者单位： | 上海大学,计算机工程与科学学院,上海,200072 |
| |
| 基金项目： | 国家自然科学基金，国家高技术研究发展计划(863计划)，国家重点基础研究发展计划(973计划)，上海市教委资助项目，上海市霞点学科建设基金 |
| |
| 摘 要： | 模型检验技术是开发高可信系统的重要途径.提出了一种基于定理证明的模型验证方法,并实现了工具验证.它以代数规约语言CafeOBJ描述系统的无限状态并把它转换成有限状态的SMV规约.通过观察迁移系统,证明产生的SMV规约的反例即CafeOBJ规约的反例,来找出开发早期阶段的系统的潜在错误,从而避免时间、金钱的耗费及重复性的劳动.
|
| 关 键 词： | 模型检测 模型验证 模型检查工具 |
Model checking analysis of observational transition system with SMV |
| |
| HE Tao,MIAO Huai-kou.Model checking analysis of observational transition system with SMV[J].Computer Engineering and Design,2008,29(18). |
| |
| Authors: | HE Tao MIAO Huai-kou |
| |
| Affiliation: | HE Tao,MIAO Huai-kou(School of Computer Engineering , Science,Shanghai University,Shanghai 200072,China) |
| |
| Abstract: | 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 speci-fication,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 proces... |
| |
| Keywords: | SMV CafeOBJ |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
