| 用高阶逻辑表达时态逻辑及其应用 |
| |
| 引用本文： | 韩俊刚.用高阶逻辑表达时态逻辑及其应用[J].计算机学报,1993,16(12):925-930. |
| |
| 作者姓名： | 韩俊刚 |
| |
| 作者单位： | 西安电子科学技术大学 西安 |
| |
| 摘 要： | 硬件设计的形式化验证技术开辟了对复杂的超大规模集成电路设计进行验证的新途径。高阶逻辑和时态逻辑在形式化验证技术中均得到成功的应用。本文介绍用高阶逻辑表达线性时态逻辑和区间时态逻辑的方法，并以几个简单实例说明它在硬件设计验证中的应用。这种方法的优点是既利用高阶逻辑系统ＨＯＬ的机械化定理证明手段，又发挥了时态逻辑的表达硬件的动态性质的能力。
|
| 关 键 词： | 硬件 设计 时态逻辑 高阶逻辑 |
EXPRESSING TEMPORAL LOGIC IN HIGHER-ORDER LOGIC AND ITS APPLICATIONS |
| |
| Han JungangXi'an University of Electronic Science,and Technology,Xi'an.EXPRESSING TEMPORAL LOGIC IN HIGHER-ORDER LOGIC AND ITS APPLICATIONS[J].Chinese Journal of Computers,1993,16(12):925-930. |
| |
| Authors: | Han JungangXi'an University of Electronic Science and Technology Xi'an |
| |
| Affiliation: | Han JungangXi'an University of Electronic Science,and Technology,Xi'an 710071 |
| |
| Abstract: | This paper presents a method of expressing linear temporal logic and interval temporal logic in higher-order logic and gives some examples of proving the correctness of simple circuits.The method takes the advantages of both mechanized HOL facilities and expressing power of temporal logic.It can be used to deal with the timing problems of VLSI system. |
| |
| Keywords: | Hardware design formal verification temporal logic higher-order logic |
| 本文献已被 CNKI 维普 等数据库收录！ |
