Automated Formal Verification at the Hardware/Software Boundary

硬件/软件边界的自动形式验证

• 批准号: RGPIN-2015-04618
• 负责人: Hu, Alan
• 金额: $ 3.13万
• 依托单位: University of British Columbia
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2019
• 资助国家: 加拿大
• 起止时间: 2019-01-01 至 2020-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=688592
• 关键词: Automated; Formal; Verification; Hardware; Software

Computer chips, computer systems, and computer software are the most complex things ever designed by humans. For example, even the simple programs written by our students in their first computer science course have far more possible behaviors than there are photons in the universe! Not surprisingly, it's hard to get all the details right. In fact, companies now spend the most effort not on design, but on verification -- the task of determining if the system behaves correctly.******Formal verification is the use of mathematical logic to aid the verification process. My research emphasizes automatic formal verification, in which a computer program analyzes the system being designed, automatically finding bugs or proving properties about the design, with minimal human effort beyond specifying what is desired. Research breakthroughs over the past twenty years have made formal verification indispensible for verifying computer hardware -- all major computer companies use formal verification on their computer chips. This has been a big success story of academic research creating enormous value for society. With more recent research breakthroughs, automated formal verification is becoming mainstream for software verification as well.******Much of the impact of computing, however, comes not from hardware or software, per se, but from actual, life-changing, "smart" products -- the smartphone being the most obvious example, but with the coming Internet of Things, all sorts of everyday objects will become smart and connected. Smart products are the result of tightly integrated hardware and software, and it's obviously important to get this integration correct. However, companies are having great difficulty creating these new products, because hardware and software have fundamentally different models of computation, resulting in mistakes when integrating the two.******This proposal focuses on developing theoretical and practical tools for verifying the interaction between hardware and software. In some respects, this combines all of the challenges of automated formal verification of hardware and software, because verification must reason about both. On the other hand, I believe that there are certain characteristics and design patterns that can be exploited to enable practical, automatic formal verification at the hardware/software boundary. If successful, this research will generate a large quality and productivity boost for creating any smart product.**

计算机芯片、计算机系统和计算机软件是人类有史以来设计的最复杂的东西。 例如，即使是我们的学生在第一门计算机科学课程中编写的简单程序，其可能的行为也远远超过宇宙中的光子！ 毫不奇怪，很难把所有的细节都做对。 事实上，公司现在花最多的精力不是在设计上，而是在验证上--确定系统是否正确运行的任务。形式验证是使用数学逻辑来辅助验证过程。 我的研究强调自动形式验证，其中计算机程序分析正在设计的系统，自动查找错误或证明设计的属性，除了指定所需的内容外，还需要最少的人力。 过去二十年的研究突破使得形式验证成为验证计算机硬件不可或缺的工具--所有主要的计算机公司都在其计算机芯片上使用形式验证。 这是学术研究为社会创造巨大价值的一个巨大成功故事。 随着最近的研究突破，自动化形式验证也成为软件验证的主流。然而，计算的大部分影响并不是来自硬件或软件本身，而是来自实际的、改变生活的“智能”产品--智能手机是最明显的例子，但随着物联网的到来，各种日常物品都将变得智能和互联。 智能产品是硬件和软件紧密集成的结果，显然，正确实现这种集成非常重要。 然而，公司在创造这些新产品时遇到了很大的困难，因为硬件和软件具有根本不同的计算模型，导致在集成两者时出现错误。该提案侧重于开发用于验证硬件和软件之间相互作用的理论和实践工具。 在某些方面，这结合了硬件和软件的自动化形式验证的所有挑战，因为验证必须考虑两者。 另一方面，我相信有一些特性和设计模式可以用来在硬件/软件边界上实现实际的自动形式化验证。 如果成功，这项研究将为创造任何智能产品带来巨大的质量和生产力提升。