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

NSF-CNPq 合作研究：工业复杂性中计算机系统的形式验证

• 批准号: 9900309
• 负责人: Edmund Clarke
• 金额: $ 15.54万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1999
• 资助国家: 美国
• 起止时间: 1999-09-01 至 2005-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9900309&HistoricalAwards=false
• 关键词: NSF; CNPq; Collaborative; Research; Formal

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.

9900309 Edmund Clark模型检查是一种用于有限状态并发系统的自动验证技术，例如时序电路设计和通信协议。 通过使用特殊的数据结构，如二元决策图，可以验证具有大量可达状态的极其复杂系统的属性。虽然这项技术已经被主要的高科技公司使用，但还需要进行更多的研究才能实现该方法的全部潜力。 目前的工具所能处理的问题的规模是有限的。 这项研究的目标之一是追求一些项目，这些项目将解决状态爆炸问题，并允许验证更大的系统，比目前可能的大许多数量级。 另一个目标是将模型检查技术扩展到目前无法直接处理的不同类型的系统。 传统上，模型检测一直应用于硬件设计，后来扩展到其他类型的系统，如实时系统。 我们相信，将模型检测应用于不同类型的系统，如随机系统，可以开辟新的研究领域，并有助于解决实际应用中的重要问题。 这项工作将与米纳斯吉拉斯州联邦大学的Sergio Campos和北格兰德河联邦大学的大卫Deharbe合作完成，他们将得到巴西CNPq的支持。