摘要
针对模型组合中常见的"状态空间爆炸"问题,分析了抽象和组合两种方法各自的优缺点,采用"反例引导的抽象精化"框架和模型检验思想,将抽象和组合结合起来,为模型组合的检验提出了一种新的方法。设计了模型的抽象、组合、检验和精化算法,开发了一款基于反例引导的、图形化的模型检验工具,使用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.
出处
《计算机工程与设计》
CSCD
北大核心
2009年第22期5041-5043,5047,共4页
Computer Engineering and Design
基金
国家自然科学基金项目(60673115)
上海市重点学科建设基金项目(J50103)
关键词
模型检验
状态爆炸
反例引导
抽象精化
抽象与组合
model checking
states explosion
counter example-guided
abstraction refinement
abstraction and composition
