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.