NSF-CNPq Collaborative Research: Formal Verification of Computer Systems in Industrial Complexity

点击翻译按钮获取中文摘要

9900309 Edmund ClarkModel checking is an automatic verification technique for finite state concurrent systems such as sequential circuit designs and communication protocols. By using special data structures like binary decision diagrams, it is possible to verify properties of extremely complex systems with immense numbers of reachable states. Although the technique is already in use by major high-tech firms, additional research is needed to realize the full potential of the method. There is a limit on the size of problems that can be handled by current tools. One of the goals of this research is to pursue a number of projects that will attack the state explosion problem and allow larger systems to be verified, some many orders of magnitude larger than currently possible. Another goal is to extend model checking techniques to different types of systems that cannot be directly handled today. Traditionally, model checking has been applied to hardware designs, being later extended to other types of systems such as real-time systems. We believe that applying model checking to different types of systems such as stochastic systems can open up new areas of research and help solve important problems with practical applications. The work will be done in collaboration with Sergio Campos of the Federal University of Minas Gerais and David Deharbe of the Federal University of Rio Grande do Norte, who will be supported by CNPq of Brazil.