欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
针对模型组合中常见的“状态空间爆炸”问题，分析了抽象和组合两种方法各自的优缺点，采用“反例引导的抽象精化”框架和模型检验思想，将抽象和组合结合起来，为模型组合的检验提出了一种新的方法。设计了模型的抽象、组合、检验和精化算法，开发了一款基于反例引导的、图形化的模型检验工具，使用Kripke结构建立模型，用LTL描述性质，从而表明了反例引导的模型检验方法的过程。
英文摘要：
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.
同期刊论文项目
同项目期刊论文
期刊信息
位置：