Efficient Model Checking of Concurrent and Dynamic Software

并发动态软件的高效模型检查

• 批准号: 0429120
• 负责人: Edmund Clarke
• 金额: --
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2004
• 资助国家: 美国
• 起止时间: 2004-10-01 至 2009-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0429120&HistoricalAwards=false
• 关键词: Efficient; Model; Checking; Concurrent; Dynamic

Software correctness is essential to avoid costly or catastrophicfailures in modern safety-critical systems, such as the ones reliedupon by NASA. Model checking is a verification technique that checksthe correctness of a system by exhaustively exploring all of itspossible behaviors. It has proven successful in the development ofhardware designs and is used by Intel and other major hardwarecompanies. Before model checking can significantly improve thereliability of mission critical software, a number of basic researchproblems must be addressed. The extraordinary complexity of realsystems results in an explosion in the possible behaviors that need tobe checked. The techniques devised to mitigate this problem forhardware can also be applied to software; however, some of the mostsuccessful ones, such as symbolic model checking, have provendifficult to apply in this new domain. The primary direction of this research is to adapt these techniques tothe task of checking concurrent software. Fundamental changes to thealgorithms are required due to the different characteristics ofhardware and software systems. Modern software systems are oftendeveloped using object-oriented languages, such as C++ and Java. Whileobject-oriented languages ease the design phase, they introduceadditional challenges for verification. One important characteristicof modern object-oriented software designs is the dynamic creation ofthreads and objects. This research aims at leveraging existingtechniques, such as the partial-order reduction and symbolic modelchecking, by extending them to address this challenge.

软件的正确性对于避免现代安全关键系统（例如 NASA 所依赖的系统）中发生代价高昂或灾难性故障至关重要。 模型检查是一种验证技术，通过详尽地探索系统的所有可能行为来检查系统的正确性。 事实证明，它在硬件设计开发方面取得了成功，并被英特尔和其他主要硬件公司所使用。在模型检查能够显着提高关键任务软件的可靠性之前，必须解决一些基础研究问题。真实系统的异常复杂性导致需要检查的可能行为激增。 为缓解硬件问题而设计的技术也可以应用于软件；然而，一些最成功的方法，例如符号模型检查，已被证明很难应用于这个新领域。这项研究的主要方向是将这些技术应用于检查并发软件的任务。 由于硬件和软件系统的不同特点，需要对算法进行根本性的改变。现代软件系统通常使用面向对象语言开发，例如 C++ 和 Java。虽然面向对象语言简化了设计阶段，但它们给验证带来了额外的挑战。现代面向对象软件设计的一个重要特征是线程和对象的动态创建。本研究旨在利用现有技术，例如偏序约简和符号模型检查，通过扩展它们来应对这一挑战。