Sciweavers

Share
ICSE
1999
IEEE-ACM

Data Flow Analysis for Checking Properties of Concurrent Java Programs

9 years 2 months ago
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.
Gleb Naumovich, George S. Avrunin, Lori A. Clarke
Added 04 Aug 2010
Updated 04 Aug 2010
Type Conference
Year 1999
Where ICSE
Authors Gleb Naumovich, George S. Avrunin, Lori A. Clarke
Comments (0)
books