Automatic Verification of Finite-State Concurrent Systems in Hardware and Software

软硬件有限状态并发系统的自动验证

• 批准号: 9803774
• 负责人: Edmund Clarke
• 金额: $ 47.5万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1998
• 资助国家: 美国
• 起止时间: 1998-07-01 至 2002-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9803774&HistoricalAwards=false
• 关键词: Automatic; Verification; Finite; State; Concurrent

9803774 Model 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 systems with extremely large numbers of reachable states. Although the technique is beginning to be used by companies like Intel, Motorola, and Siemens, additional research is needed to realize the full potential of the method. This project will develop a number of new techniques that should enable larger hardware systems and certain types of software systems such as security protocols and probabilistic programs to be verified. The new techniques involve extending the partial order reduction to permit symbolic model checking of real-time programs, combining model checking and theorem proving, using program slicing to reduce the state explosion problem in model checking, and combining abstraction with binary decision diagrams.***

9803774 模型检查是一种用于有限状态并发系统（例如时序电路设计和通信协议）的自动验证技术。通过使用二元决策图等特殊数据结构，可以验证具有大量可达状态的系统的属性。 尽管英特尔、摩托罗拉和西门子等公司已开始使用该技术，但仍需要进行更多研究才能充分发挥该方法的潜力。该项目将开发许多新技术，使更大的硬件系统和某些类型的软件系统（例如安全协议和概率程序）能够得到验证。新技术包括扩展偏序约简以允许实时程序的符号模型检查、将模型检查和定理证明相结合、使用程序切片来减少模型检查中的状态爆炸问题以及将抽象与二元决策图相结合。***