Data Flow Analysis for Checking Properties of Concurrent Java Programs

In this paper we show how the FLAVERS data flow analysis technique, originally formulated for programs with the rendezvous model of concurrency, can be applied to concurrent Java programs. The general approach of FLAVERS is based on modeling a concurrent program as a flow graph and using a data flow analysis algorithm over this graph to check statically if a property holds on all executions of the program. The accuracy of this analysis can be improved by supplying additional information, represented as finite state automata, to the data flow analysis algorithm. In this paper we present a straightforward approach for modeling Java programs that uses the accuracy improving mechanism to represent the possible communications among threads in Java programs, instead of representing them directly in the flow graph model. We also discuss a number of error-prone thread communication patterns that can arise in Java and describe how FLAVERS can be used to check for the presence of these.

• Type: Conference
• Year: 1999
• Where: ICSE
• Authors: Gleb Naumovich, George S. Avrunin, Lori A. Clarke
• Keywords: Analysis Algorithm, Data flow Analysis, ICSE 1999, Java Programs, Software Engineering