Efficient Model Checking of Concurrent and Dynamic Software

Carnegie Mellon University, Pittsburgh PA

Investigators

Abstract

Software correctness is essential to avoid costly or catastrophic failures in modern safety-critical systems, such as the ones relied upon by NASA. Model checking is a verification technique that checks the correctness of a system by exhaustively exploring all of its possible behaviors. It has proven successful in the development of hardware designs and is used by Intel and other major hardware companies. Before model checking can significantly improve the reliability of mission critical software, a number of basic research problems must be addressed. The extraordinary complexity of real systems results in an explosion in the possible behaviors that need to be checked. The techniques devised to mitigate this problem for hardware can also be applied to software; however, some of the most successful ones, such as symbolic model checking, have proven difficult to apply in this new domain. The primary direction of this research is to adapt these techniques to the task of checking concurrent software. Fundamental changes to the algorithms are required due to the different characteristics of hardware and software systems. Modern software systems are often developed using object-oriented languages, such as C++ and Java. While object-oriented languages ease the design phase, they introduce additional challenges for verification. One important characteristic of modern object-oriented software designs is the dynamic creation of threads and objects. This research aims at leveraging existing techniques, such as the partial-order reduction and symbolic model checking, by extending them to address this challenge.