Temporal Logic, Hardware Verification, and Automatic Theorem Proving

时态逻辑、硬件验证和自动定理证明

• 批准号: 8722633
• 负责人: Edmund Clarke
• 金额: $ 15.84万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1988
• 资助国家: 美国
• 起止时间: 1988-03-01 至 1990-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=8722633&HistoricalAwards=false
• 关键词: Temporal; Logic; Hardware; Verification; Automatic

This work comprises several research projects in logics of programs and program verification. All of the projects are directed towards providing tools that will make automatic verification feasible for a wider class of programs. The first three projects involve an approach to verifying finite state concurrent systems called temporal logic model checking. This procedure will determine if a finite-state concurrent system satisfies its specification in a propositional temporal logic by methodically searching the global state graph generated by the concurrent system. It has been used successfully to find subtle errors in published designs of tricky self-timed circuits. The first project is to develop ways of handling the state explosion problem that may occur with this type of verification. Another project is to extend the temporal logic and its verification procedure to allow operators defined by automata on infinite tapes. This is of practical importance since a frequent criticism of temporal logic is its expressive power compared to automata. The third project involves actually using model checking techniques for the automatic verification of hardware controllers. The main problem in this case is to develop methods of extracting state machines from circuits under realistic timing models. The last project is the development of a parallel resolution theorem prover to run on Sequent and Encore multiprocessors. It is already well underway. Since interest primarily in problems caused by concurrency, one can use a fairly simple theorem proving strategy based on linear resolution/model elimination. Clauses are maintained according to some heuristic function in a heap data structure that permits parallel inserts and deletions. A prototype implementation of the full system should be running in the next few months. Experiments with other ways of organizing the theorem prover and with more complicated theorem proving strategies will follow.

这项工作包括程序逻辑的几个研究项目， 程序验证 所有的项目都是针对 提供使自动核查可行的工具， 更广泛的课程。 前三个项目涉及一种验证有限状态的方法 并发系统称为时态逻辑模型检查。 这 过程将确定有限状态并发系统是否满足 它在命题时态逻辑中的规范， 搜索由所述并发系统生成的所述全局状态图。 它已被成功地用于发现出版物中的细微错误 复杂的自定时电路设计。 第一个项目是开发 处理可能发生的状态爆炸问题的方法 验证的类型。 另一个项目是扩展时态逻辑 和它的验证过程，允许由自动机定义的算子 无限的磁带。 这一点具有重要的实际意义，因为 时间逻辑的批评是它的表达能力相比， 自动机 第三个项目涉及实际使用模型检查 硬件控制器的自动验证技术。 的 在这种情况下，主要问题是开发提取状态的方法 机器从电路下现实的定时模型。 最后一个项目是并行归结定理的发展 在Sequent和Encore多处理器上运行。 已经是 顺利进行中。 由于兴趣主要是由 并发，可以使用一个相当简单的定理证明策略， 线性分辨率/模型消除。 条款被保留 根据堆数据结构中的某个启发式函数， 允许并行插入和删除。 一个原型实现 整个系统应可在未来数月内运作。 实验 与其他组织定理证明器的方法以及更多 复杂的定理证明策略将随之而来。