Static Analysis of Concurrent Systems

Overview »

FLAVERS

INCA

Propel

Verification Examples

Publications

Related Research

Perpetual Testing

Verification Examples

Introduction

Society is increasingly dependent upon high assurance software systems. The growing size and complexity of such systems and their reliance upon such features as concurrency and distribution creates new concerns and challenges. Traditional approaches such as testing (which can only sample a small fraction of the input space) and theorem proving (which requires extensive human expertise) are inadequate. In LASER we are investigating alternative high assurance approaches, based on finite state verification, that are computationally tractable, easy to use, and applicable to a wide class of properties.

The goal of software analysis research in LASER is to develop practical techniques that can help software developers determine whether software systems satisfy their requirements. The focus of most of our research is on the static analysis of concurrent software--the nondeterministic behavior introduced by concurrency means that dynamic analysis (testing) is not adequate for concurrent systems. Since concurrent systems are built of interacting sequential components, however, many of the techniques we use for analyzing concurrent systems can also be applied to sequential software.

Our work focuses on two on-going projects: FLAVERS, which uses data flow analysis to verify properties, and INCA, which uses integer linear programming to verify properties.

Empirical Evaluation of Analysis Methods and Tools

A number of techniques have been proposed for static concurrency analysis. These techniques include reachability analysis, which generates the state space of the concurrent program and checks the property of interest on that state space; symbolic model checking, which checks the property on a symbolic representation of the state space; integer programming, which specifies the program and property as a system of integer inequalities and looks for a solution to that system; and dataflow analysis, which checks the property by solving a dataflow problem on a graphical representation of the program. For each of the techniques, one or more tools have been developed to implement the technique.

Unfortunately, there is little information available to help analysts choose between the analysis tools. In general, all the techniques take exponential time in the worst case, but little is known about average case analysis time or the consumption of other resources. Furthermore, to ensure that the analysis is conservative or to improve tractability, in practice most of the techniques overestimate the behavior of the program being analyzed. This overestimate can lead to a tool falsely reporting that a property may be violated. Thus, accuracy of the analysis is another important dimension on which the techniques must be evaluated.

We have carried out a comparison of several static analysis tools, applying the tools to a number of concurrent Ada programs from the analysis literature. We are now beginning a much larger project involving a combination of analysis of several large real programs and experiments with special programs constructed to isolate particular features identified in the analysis of the real programs as having significant impact on the utility of the analysis tools. As a pilot study for that project, we have begun analyzing the Chiron user interface development system from the University of California, Irvine, using the INCA and FLAVERS tools. This analysis has, for example, identified a deadlock that had been observed but not isolated in some applications of Chiron.

Other LASER Analysis Research

Other analysis research in LASER involves such topics as:

• Compositional analysis, which analyzes subsystems separately and combines the results of those analyses to obtain results about a large system.
• The application of mathematical techniques to improve analysis, including the use of computational algebraic geometry in symbolic model checking and making better use of symmetry groups to improve the tractability of analysis.
• Analysis of software architectures, applying analysis methods for concurrent programs to software architectures.
• Application of static analysis to formally specified processes.

© 2006 University of Massachusetts Amherst. Site Policies.
This site is maintained by the Laboratory for Advanced Software Engineering Research.