Simultaneous reachability analysis of concurrent systems

Concurrent systems constitute a major part of the computing systems today. These systems are built from smaller components or processes that operate concurrently and communicate with each other. Understanding the overall behavior of these systems is a challenging task due to the non-determinism of interactions between different processes. Increase in the size and the number of processes in a concurrent system further complicates the analysis of the system. This dissertation addresses the problem of performing scalable analysis of concurrent systems.; General approaches to analysis of concurrent systems include automated techniques such as reachability analysis and model checking. Reachability analysis involves systematically generating all reachable states of a concurrent system to detect deadlocks and other types of faults. Model checking involves specifying desirable properties for a concurrent system as temporal logic formulas and verifying that these formulas are satisfied by the reachable states of the system. The state explosion problem restricts the scalability of these methods. In the worst case the number of generated states grows exponentially with the number of processes in the system.; In this dissertation we present general solutions to alleviate the state explosion problem in reachability analysis and model checking. Our solutions aim to explore only a small portion of all reachable states of a concurrent system in order to determine whether the system satisfies certain properties. Our approach is based on a technique called simultaneous reachability analysis (SRA). The main idea behind SRA is to permit a global transition in a reachability graph to contain a set of local transitions (i.e. transitions of individual processes) such that the state reached by the global transition is independent of the execution order of the associated local transitions.; We present an algorithm for applying the SRA idea to perform deadlock analysis of an asynchronous system. Empirical studies indicate that our SRA algorithm significantly reduces the number of states generated during reachability analysis.; We describe an SRA-based framework for producing a reduced reachability graph that provides sufficient information for model checking. We present an SRA-based algorithm for model checking of concurrent systems. Empirical results indicate that our algorithm generates significantly reduced reachability graphs for model checking.; In order to apply reachability analysis or model checking to a concurrent system, it is necessary to determine the number of instances of each process type in the system. Different versions of a concurrent system, obtained by varying the number of process instances in the system, may have different types of faults. It is desirable to find a version of a concurrent system such that if this version is fault-free, then all other versions of the system that have more process instances are either likely or guaranteed to be fault-free. This problem is referred to as the instance upper bound problem.; In this dissertation we present a heuristic solution to the instance upper bound problem. We assume that a set of sequencing constraints exists for a concurrent system. Based on the criterion of covering each sequencing constraint once, we show how to determine the number of instances of each process type in a concurrent system such that the total number of process instances is minimum.