Donald Bren School of Information and Computer Sciences

Analysis is essential for validation of reliable software systems. This is especially important for concurrent (multitasking) systems because their nondeterministic behaviors compound the difficulties of other means of assurance, such as testing. Unfortunately, conventional concurrent program design methodologies do not address analyzability, and the structural features that affect analyzability are not adequately identified. Therefore, many concurrent systems are not structured to be analyzable with conventional techniques and tools. Moreover, designers often do not know to what extent their systems are analyzable without actually attempting full-scale analysis.

Static concurrency analysis can guarantee freedom from anomalies such as deadlock, dangerous access to shared variables, and undesired temporal properties. For example, exhaustive enumerative techniques such as reachability analysis are powerful and conceptually appealing. These benefits offer strong incentives to, in particular, restructure any given system for analysis and to, in general, adapt development processes to address analyzability earlier in the lifecycle. However, these techniques suffer from state-space explosion and therefore have limited utility for analyzing complex real-world systems.

This dissertation describes a practical approach for evaluating the analyzability of the concurrency structure of existing software systems. A key feature of this metric-driven evaluation approach is that it identifies specifically the complex structural features of the system, and thereby provides guidance for restructuring the system to enhance its analyzability. Results of the successful application of this approach to several actual systems are reviewed. Beyond restructuring of-existing systems, the approach offers sufficient structural characterization to support the augmentation of concurrent program design methodologies. Thus, the analyzability of resulting designs and systems can be enhanced in a systematic, metric-driven manner.