| 反例引导的模型检验工具的设计 |
| |
| 引用本文： | 谭亮,曾红卫.反例引导的模型检验工具的设计[J].计算机工程与设计,2009,30(22). |
| |
| 作者姓名： | 谭亮 曾红卫 |
| |
| 作者单位： | 上海大学,计算机工程与科学学院,上海,200072 |
| |
| 基金项目： | 国家自然科学基金项目，上海市重点学科建设基金项目 |
| |
| 摘 要： | 针对模型组合中常见的"状态空间爆炸"问题,分析了抽象和组合两种方法各自的优缺点,采用"反例引导的抽象精化"框架和模型检验思想,将抽象和组合结合起来,为模型组合的检验提出了一种新的方法.设计了模型的抽象、组合、检验和精化算法,开发了一款基于反例引导的、图形化的模型检验工具,使用Kripke结构建立模型,用LTL描述性质,从而表明了反例引导的模型检验方法的过程.
|
| 关 键 词： | 模型检验 状态爆炸 反例引导 抽象精化 抽象与组合 |
Counter example-guided design of model checking tool |
| |
| TAN Liang,ZENG Hong-wei.Counter example-guided design of model checking tool[J].Computer Engineering and Design,2009,30(22). |
| |
| Authors: | TAN Liang ZENG Hong-wei |
| |
| Affiliation: | TAN Liang,ZENG Hong-wei(School of Computer Engineering and Science,Shanghai University,Shanghai 200072,China) |
| |
| Abstract: | To solve "states explosion", which is a common problem in model composition, the advantages and disadvantages of abstraction and composition are analyzed. And they are combined by using the "counter example-guided abstraction refinement" fra-mework and model checking. A new method for the verification of model composition is proposed and the algorithms of model' s abstrac-tion, composition, verification and refinement are designed. A GUI checking tool is developed, Kripke is used to build the model and LTL is used to describe the property, the peocess of model checking based on counter example is explained. |
| |
| Keywords: | model checking states explosion counter example-guided abstraction refinement abstraction and composition |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
