Abstração de Processos
Infinitos em CSPZ: Tratando
Comunicação e Instabilidade
Aluno: Adalberto Cajueiro de Farias
Orientador: Alexandre Mota
Co-Orientador: Augusto Sampaio
Motivação
Explosão de estados de processos CSPZ
Usar abstração de dados para evitar o
problema da explosão de estados


Baseada em propriedades
Independente de propriedades
Mecanizar a estratégia através de um
algoritmo baseado em



Estabilidade
Independência de dados
Interpretação abstrata e Refinamento de dados
inverso
Exemplo
Model checking de CSPZ
Abstração de Dados
Abstração de Dados
Algoritmo
Considera ambas partes comportamental e de
dados durante a expansão
Não captura aspectos de inicialização
Não lida com valores comunicados nos canais
Não lida com processos instáveis
Permite construções complexas na parte de
Z, o que pode dificultar bastante o passo de
prova de teoremas
Proposta de Trabalho
Estender a classe de problemas tratáveis pelo
algoritmo





Capturar aspectos de inicialização
Lidar com valores comunicados nos canais
Lidar com processos instáveis
Limitar a lógica permitida na parte de Z, ou usar
outra linguagem baseada em modelos que permita
prova de teoremas mais automática
Ferramenta de apoio
Cronograma
Abordagens Relacionadas
A. Mota. Model checking CSPZ: Techniques to overcomes the
state explosion problem (2001)
A. Farias. Efficient and Mechanised Analysis of Infinite CSPZ
Specifications: strategy and tool support (2003)
Christie, B. and Davies, J. and Woodcock, J. On the Refinement
and Simulation of Data Types and Processes (1999)
Smith, G. and Winter, K. Proving temporal properties of Z
specifications using abstraction (2003)
Isobe, Y. and Roggenbach, M. A generic theorem prover of CSP
refinement (2005)
T. Ball et. Al. SLAM and Static Driver Verifier: Technology
Transfer of Formal Methods inside Microsoft (2004)