Reachability analysis and testing of asynchronous message-passing programs.

摘要

An asynchronous message-passing program consists of concurrent processes that interact with each other by the exchange of messages. Many network protocols and distributed applications are asynchronous message-passing programs. This dissertation investigates techniques to ensure correctness of asynchronous message-passing programs.; Reachability analysis has been a successful approach to verifying concurrent programs. Existing reachability analysis techniques for asynchronous message-passing programs assume causal communication, which means that messages sent to a destination are received in the order they are sent. In the first part of this dissertation, we propose a new reachability analysis approach, called blocking-based simultaneous reachability analysis (BSRA), for asynchronous message-passing programs based on any communication scheme. We describe an algorithm for generating BSRA-based reachability graphs and show that this algorithm guarantees the detection of deadlocks. Empirical results indicate that BSRA significantly reduces the number of states in reachability graphs.; The second part of this dissertation deals with a new concept of testing concurrent programs, namely reachability testing. Let P be an asynchronous message-passing program, and X an input of P. Assume that every execution of P with X terminates. Reachability testing of P with X is to execute, in a systematic manner, all possible synchronization sequences (or SYN-sequences) of P with X such that the correctness of P with X can be determined. The main challenge of reachability testing is to derive race variants of SYN-sequences. We develop a formal approach to computing race variants of SYN-sequences consisting of send and receive events. We describe an efficient reachability testing algorithm for asynchronous message-passing programs.; In the third part of this dissertation, we propose a new test generation strategy, called In-Parameter-Order (or IPO), for pairwise testing. Pairwise testing requires that for each pair of input parameters of a system, every combination of valid values of these two parameters be covered by at least one test case. For a system with two or more input parameters, the IPO strategy generates a pairwise test set for the first two parameters, extends the test set to generate a pairwise test set for the first three parameters, and continues to do so for each additional parameter. We present IPO-based test generation algorithms. We describe an IPO-based test generation tool and show some empirical results.