Automatic Verification of Finite-State Concurrent Systems in Hardware and Software

软硬件有限状态并发系统的自动验证

• 批准号: 9217549
• 负责人: Edmund Clarke
• 金额: $ 74.49万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1993
• 资助国家: 美国
• 起止时间: 1993-05-15 至 1998-10-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9217549&HistoricalAwards=false
• 关键词: Automatic; Verification; Finite; State; Concurrent

Logical errors in sequential circuit designs and communication protocols have always been an important problem. They can delay getting a new product on the market or cause the failure of some critical device that is already in use. The most widely used method for verifying such systems is based on extensive simulation and can easily miss significant errors when the number of possible states is very large. This research deals with developing an alternative approach based on a technique called temporal logic model checking. In this approach specifications are expressed in a propositional temporal logic, and sequential circuits and communication protocols are modeled as state transition systems. An efficient search procedure is used to determine automatically if the specifications are satisfied by the transition system. The technique has been used in the past to find subtle errors in a number of non-trivial designs.

时序电路设计和通信协议中的逻辑错误一直是一个重要问题。它们可能会延迟新产品上市，或导致一些已在使用的关键设备出现故障。最广泛使用的验证此类系统的方法是基于广泛的模拟，当可能的状态数量非常大时，很容易错过重大错误。 这项研究涉及开发一种替代方法的基础上，称为时序逻辑模型检查的技术。 在这种方法中，规范表示在一个命题时序逻辑，时序电路和通信协议建模为状态转移系统。 一个有效的搜索过程是用来自动确定的规格是否满足过渡系统。 该技术已被用于在过去发现一些非平凡的设计中的细微错误。