A Verification Manager for Adaptive Model Checking

用于自适应模型检查的验证管理器

• 批准号: 9971195
• 负责人: Fabio Somenzi
• 金额: $ 47.68万
• 依托单位: University of Colorado at Boulder
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1999
• 资助国家: 美国
• 起止时间: 1999-10-01 至 2002-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9971195&HistoricalAwards=false
• 关键词: Verification; Manager; Adaptive; Model; Checking

With verification taking about two thirds of the development cycle, formalmethods hold great promise of increasing the productivity of electronicdesigners. To overcome the limitations of current formal verificationalgorithms, this project explores adaptive model checking techniques. Modelchecking is a technique for the verification of properties of finite statesystems. Application of model checking to large systems is hindered by theexponential growth of the number of states with the number of statevariables---a problem known as state explosion. This project addresses thestate explosion problem by a combination of three approaches: verificationmanagement, automatic abstraction/refinement, and binary decision diagram(BDD) technology. These approaches combine to give adaptive model checking,in which the verification management component identifies the appropriatepartitioning and abstraction strategies and extracts from the design to beverified information that guides BDD-based algorithms to efficient symbolicstate exploration.

由于验证约占开发周期的三分之二，形式方法在提高电子设计人员的生产力方面有很大的潜力。为了克服现有形式化验证算法的局限性，本项目探索了自适应模型检测技术。模型检测是一种验证有限状态系统性质的技术。模型检测在大系统中的应用受到状态数随状态变量数呈指数增长的阻碍--一个被称为状态爆炸的问题。本计画结合验证管理、自动化抽象/精化及二元决策图技术来解决状态爆炸问题。这些方法联合收割机给出自适应模型检测，其中验证管理组件识别适当的划分和抽象策略，并从设计中提取待验证的信息，指导基于BDD的算法进行有效的符号状态探索。