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

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

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.