U.S.-Japan Cooperative Research: Formal Verification of Finite State Systems

该奖项为一个为期两年的研究项目提供支持 Edmund Clarke教授，计算机科学学院， 卡内基梅隆大学教授Hiromi Hiraishi 日本京都大学情报科学系。 该项目的目的是研究形式验证 有限状态系统的方法 这些系统出现 在计算机软件和通信的设计中， 协议，它们的正确性很可能成为一个 未来的重要问题。 最近的研究表明， 有限系统通常可以自动验证， 建立和分析系统的状态图模型 行为 然而，这些方法依赖于决策算法 它明确地构建了状态图模型， 模型中的状态数量可以指数增长， 并发执行组件的数量、复杂性 可以验证的系统数量有限。 这 研究将集中在避免这种情况的新技术上 问题，因此形式验证可以应用于 现实复杂性的系统。 许多替代 技术已经提出。 一个例子是利用 验证中电路的层次结构 过程 每个单独的组件可以单独验证 并将结果结合起来， 系统的行为。 第二种方法是实施 可以在超级计算机上运行的并行算法。 参与该项目的美国和日本研究人员 一直在开发检测这些设计的技术 错误和最近的研究都提供了强有力的证据 有可能为此开发出实用的工具， 目的. 两位研究者的研究技巧是 互补，每个国家都有很多东西可以学习， 其他关于处理这个问题的方法。 如果成功 该项目将导致自动化的新技术， 有限状态系统的设计验证。

This award provides support for a two year research project between Professor Edmund Clarke, School of Computer Science, Carnegie Mellon University, and Professor Hiromi Hiraishi, Department of Information Science, Kyoto University, Japan. The aim of the project is to investigate formal verification methods for finite state systems. These systems arise naturally in the design of computer software and communication protocols, and their correctness is likely to become an important issue in the future. Recent work has shown that finite systems can often be verified automatically by constructing and analyzing state-graph models of system behavior. However these methods rely on decision algorithms which explicitly construct the state-graph model and because the number of states in a model may grow exponentially with the number of concurrently executing components, the complexity of systems that can be verified has been limited. This research will focus on new techniques which avoid this problem, so that formal verification can be applied to systems of realistic complexity. A number of alternative techniques have been proposed. One example is to exploit the hierarchical structure of the circuit in the verification process. Each individual component may be verified separately and the results combined to infer properties of the global behavior of the system. A second approach is to implement parallel algorithms that will run on supercomputers. Both the US and Japanese researchers involved in this project have been developing techniques for detecting these design errors and recent research by both provides strong evidence that it is possible to develop practical tools for this purpose. The research skills of the two researchers are complementary and each country has much to learn from the other about ways of dealing with this problem. If successful this project should lead to new techniques for automatic design verification of finite state systems.