Hybrid verification integrating HOL theorem proving with MDG model checking

Rabeb Mizouni; Sofiene Tahar; Paul Curzon

首页> 外文期刊>Microelectronics journal >Hybrid verification integrating HOL theorem proving with MDG model checking

【24h】

Hybrid verification integrating HOL theorem proving with MDG model checking

机译：结合了HOL定理证明和MDG模型检查的混合验证

获取原文

获取原文并翻译 | 示例

掌桥外文数据库（机构版） >>

开具论文收录证明 >>

文献代查 >>

页面导航

摘要
著录项
相似文献
相关主题

摘要

In this paper, we describe a hybrid tool for hardware formal verification that links the HOL (higher-order logic) theorem prover and the MDG (multiway decision graphs) model checker. Our tool supports abstract datatypes and uninterpreted function symbols available in MDG, allowing the verification of high-level specifications. The hybrid tool, HOL-MDG, is based on an embedding in HOL of the grammar of the hardware modeling language, MDG-HDL, as well as an embedding of the first-order temporal logic L_(mdg) used to express properties for the MDG model checker. Verification with the hybrid tool is faster and more tractable than using either tools separately. We hence obtain the advantages of both verification paradigms.

机译：在本文中，我们描述了一种用于硬件形式验证的混合工具，该工具链接了HOL（高阶逻辑）定理证明者和MDG（多路决策图）模型检查器。我们的工具支持MDG中提供的抽象数据类型和未解释的功能符号，从而可以验证高级规范。混合工具HOL-MDG基于硬件建模语言MDG-HDL的语法在HOL中的嵌入，以及用于表达硬件特性的一阶时间逻辑L_（mdg）的嵌入。 MDG模型检查器。与单独使用这两种工具相比，使用混合工具进行的验证更快，更容易处理。因此，我们获得了两种验证范例的优势。

著录项

来源
《Microelectronics journal》 |2006年第11期|p.1200-1207|共8页
作者
Rabeb Mizouni; Sofiene Tahar; Paul Curzon;
展开▼
作者单位

Department of Electrical and Computer Engineering, Concordia University, Montreal, Que., Canada H3G 1M8;

展开▼
收录信息美国《科学引文索引》(SCI);美国《工程索引》(EI);
原文格式 PDF
正文语种 eng
中图分类微电子学、集成电路（IC）;
关键词
multiway decision graphs (MDG); higher-order logic (HOL);

机译：多路决策图（MDG）;高阶逻辑（HOL）;

相似文献

外文文献
中文文献
专利

1. Efficiently Checking Propositional Refutations In Hol Theorem Provers [J] . Tjark Weber, Hasan Amjad Journal of Applied Logic . 2009,第1期

机译：有效地检验Hol定理证明中的命题反驳
2. Combination of Model Checking and Theorem Proving to Develop and Verify Embedded Software [J] . Zhong Xu, Xiao Jianyu Information Technology Journal . 2008,第4期

机译：结合模型检验和定理证明来开发和验证嵌入式软件
3. Combination of Model Checking and Theorem Proving to Develop and Verify Embedded Software [J] . Zhong Xu, Xiao Jianyu Information Technology Journal . 2008,第4期

机译：结合模型检验和定理证明来开发和验证嵌入式软件
4. Hybrid tool integrating HOL theorem proving with MDG model checking [C] . Mizouni, R., Tahar, . 2004

机译：结合了HOL定理证明和MDG模型检查的混合工具
5. The verification of MDG algorithms in the HOL theorem prover [D] . Abed, Sa'ed Rasmi H. 2008

机译：HOL定理证明者中MDG算法的验证
6. Petri Net and Probabilistic Model Checking Based Approach for the Modelling, Simulation and Verification of Internet Worm Propagation [O] . Misbah Razzaq, Jamil Ahmad 2010

机译：基于Petri网和概率模型检查的Internet蠕虫传播建模，仿真与验证方法。
7. The verification of MDG algorithms in the HOL theorem prover [O] . Abed Saed Rasmi H 2008

机译：HOL定理证明者中MDG算法的验证
8. Proof-Checking, Theorem Proving, and Program Verification. [R] . Boyer, R. S., Moore, J. S. 1983

机译：证明检验，定理证明和程序验证。

Hybrid verification integrating HOL theorem proving with MDG model checking

摘要

著录项

相似文献

相关主题

期刊订阅