With the proliferation of concurrent software systems, automated finite state verification techniques for checking that a software system conforms to a behavior specification become extremely important in improving software quality. Such techniques can be used both for detecting faults of certain kinds and proving that such faults are absent from the given software system. In this thesis, we adapt the promising approach of FLAVERS, a data flow analysis-based finite state verification technique, to the analysis of concurrent Java programs. We investigate two alternative approaches to modeling Java concurrency with FLAVERS and demonstrate experimentally that one of these two approaches is more efficient. In addition, we present three general optimizations of the general approach of FLAVERS. One of these optimizations improves the space requirements of the FLAVERS analysis by about an order of magnitude and all three optimizations combined reduce the analysis time approximately in half. Finally, we describe three case studies evaluating the applicability of FLAVERS to several application domains: communication protocols, high-level software architectures, and user interfaces. We demonstrate that FLAVERS is an efficient tool for detecting faults or proving the absence of faults of certain kind in these domains. We also describe two polynomial data flow algorithms for computing a conservative estimate of which pairs of statements may execute in parallel in concurrent programs. One of these algorithms computes such pairs for concurrent Ada programs and the other algorithm computes such pairs for concurrent Java programs. The empirical comparison of each of the algorithms with a precise exponential-time algorithm shows that our algorithms are very precise in practice. In addition, we compare our algorithm for Ada with the most precise of the previously proposed approaches. It turns out that our algorithm tends to be more precise in practice.
| Identifer | oai:union.ndltd.org:UMASS/oai:scholarworks.umass.edu:dissertations-3275 |
| Date | 01 January 1999 |
| Creators | Naumovich, Gleb N |
| Publisher | ScholarWorks@UMass Amherst |
| Source Sets | University of Massachusetts, Amherst |
| Language | English |
| Detected Language | English |
| Type | text |
| Source | Doctoral Dissertations Available from Proquest |
Page generated in 0.0015 seconds