Efficient Model Checking of Concurrent and Dynamic Software

在现代安全关键系统中，软件的正确性对于避免代价高昂或灾难性的故障至关重要，比如美国国家航空航天局（NASA）所依赖的系统。模型检查是一种验证技术，它通过详尽地探索系统所有可能的行为来检查系统的正确性。它已被证明在硬件设计的开发中是成功的，并被英特尔和其他主要硬件公司使用。在模型检查能够显著提高关键任务软件的可靠性之前，必须解决一些基础研究问题。现实系统的异常复杂性导致需要检查的可能行为激增。为减轻硬件问题而设计的技术也可以应用于软件；然而，一些最成功的方法，如符号模型检查，已被证明难以应用于这个新领域。本研究的主要方向是将这些技术应用于并发软件的检测任务。由于硬件和软件系统的不同特性，需要对算法进行根本性的改变。现代软件系统通常使用面向对象的语言开发，如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.