Verificando Propriedades
de Programas Concorrentes
em Java
Sérgio Soares
Flavers - FLow Analysis for
VERification of Systems
Sistemas concorrentes como um grafo de
fluxo
Análise de fluxo de dados
Flavers - FLow Analysis for
VERification of Systems
Inicialmente implementado para Ada
programas vistos como grafos de fluxo de
traces (TFG)
componentes do programa vistos como
grafos de fluxo de controle (CFG)
o TFG é a composição dos CFGs de cada
componente do sistema
Criando CFGs
task body T1 is
begin
p1;
T2.E;
end T1;
task body T2 is
begin
p2;
accept E;
p3;
end T2;
initial
initial
p2
p1
E
E
final
p3
final
Criando o TGF
initial
p1
rendezvous
p2
MIP (interleaving)
E
p3
final
Fluxo de execução
Verificando propriedades
Propriedades descritas por FSA
1
p1
p3
2
p1
p3
4
p1,p3
3
p1,p3
Verificando propriedades
Uma propriedade se verifica para um
programa se:
a projeção da linguagem do TFG no alfabeto
da propriedade está contida na linguagem da
propriedade
Data Flow analysis
verificar incrementalmente que autômatos
verificam propriedades de cada nó de execução do
TFG.
Traces inválidos
(infeasible paths )
initial
p1
p2
Exemplo de trace inválido:
initial, p1, E, final
E
p3
final
Removendo traces inválidos
Definição de FSAs que modelem restrições
semânticas na execução do programa,
não contempladas pelo TFG
remover infeasible paths (traces não
executáveis)
Feasibility constraint
1
p2
2
E
3
p3
4
E,p2
p2,p3
E,p2,p3
E,p3
v
E,p2,p3
Flavers para Java
Modelos de comunicacao
baseados em monitores (Java)
rendezvous (Ada e CSP)
Feasibility constraints representam
interações entre threads
interações entre componentes (threads) não
estão representadas no TFG como em ADA
Criando TFGs para
programas em Java
Um CFG para cada thread
Compor os CFGs com os possíveis
interleavings formando o TFG
labels na forma:
(object, method, thread)
(*, method, thread)
(object, *, thread)
(object, method, *)
Criando TFGs para
programas em Java
Exemplo de Constraint
Referências
Gleb Naumovich, George S. Avrunin, and Lori A.
Clarke. Data Flow Analysis for Checking Properties
of Concorrent Java Programs. In 21st International
Conference on Software Engineering, pages 399410. ACM press Los Angeles, California, USA, May
1999.