Efficient Model Checking of Concurrent and Dynamic Software

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

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.