1. Apresentar como se pode estender a técnica de verificação de modelos (model checking) em CSP_Z - uma linguagem formal que integra a álgebra de processos CSP com a notação baseada em modelos Z - para lidar com processos cujo espaço de estados é infinito. A verificação de modelos é baseada numa estratégia de conversão de CSP_Z para CSP puro de forma a tornar possível o reuso da ferramenta FDR (Failures Divergences Refinement) na verificação de especificações CSP_Z [Mota e Sampaio, 2001].

Figura 1: Conversão de  CSP_Z para CSP puro

Na estratégia de conversão, a parte de CSP (comportamental) é convertida em um processo controlador (mestre) e a parte de Z é convertida em um processo escravo, que faz a manipulação dos dados e mudança de estado. Ao final, ambos processos interagem através de sincronização (ver Figura 1).

2. Devido à habilidade natural em lidar com tipos de dados infinitos, CSP_Z normalmente gera sistemas infinitos, os quais não nos permite aplicar a técnica de verificação de modelos diretamente. Através da investigação desse problema, uma técnica auxiliar de compressão de dados foi proposta por [Mota et al., 2002] para lidar com sistema cujo espaço de estados é infinito. Essa estratégia é baseada na integração de duas abordagens diferentes: Independência de Dados [Lazic, 1999] e Interpretação Abstrata [Cousot e Cousot, 1992].

Além de lidar com uma linguagem que integra comportamento (CSP) e dados (Z), a abordagem de Mota [Mota et al., 2002] possui uma característica especial: a abstração de uma especificação original, a partir de sub-tipos dos tipos (infinitos) originais é gerada automaticamente a partir da análise da parte de dados (Z) da especificação original.

Estendendo essa estratégia, a nossa abordagem para abstração de dados em CSP_Z também considera a parte comportamental (CSP) quando na geração da abstração. Isso tem levado às seguintes contribuições imediatas:

1. Captura de situações específicas da parte de CSP tais como deadlock, terminação normal e divergência.

2. Maior rapidez no algoritmo na busca de abstrações. Isso se deve ao fato de que a parte de CSP funciona como um filtro da parte de Z, ou seja, nem todas as possibilidades da parte de Z precisam ser exploradas, como era feito em [Mota et al. 2002].

3. Aumento da classe de problemas tratados pela estratégia. Considerando também a parte de CSP, o nosso algoritmo é capaz de lidar com uma classe de problemas maior, cuja influência da parte de CSP importa no comportamento do processo.

4. Devido ao item 3, nosso algoritmo pode ser aplicado a mais situações. Por exemplo, alguns processos possuem a parte de Z instável. Na abordagem de [Mota et al. 2002] o algoritmo não pararia e não produziria a abstração ótima. Entretanto, na nossa abordagem, dependendo da parte comportamental do processo, o algoritmo pode parar e calcular a abstração, inclusive, de forma mais eficiente que em [Mota et al. 2002].

3. Com o intuito de estimular a aplicação da técnica de abstração de dados na prática, nosso trabalho também contribui através de uma ferramenta Java com suporte para abstração de processos CSP_Z. A ferramenta é uma evolução do protótipo apresentado em [Farias 2000] e [Farias 2001], cujo propósito era apenas dar suporte para a conversão de especificações CSP_Z em CSP puro de forma semi-automática. A Figura 2 mostra a tela principal da ferramenta, onde é possível editar um processo CSP_Z concreto (possivelmente infinito), abstrair o processo original (gerando um processo abstrato) e derivar o CSP puro para ambos processos concreto e abstrato.

Figura 2: Tela principal da ferramenta

É importante salientar que, quando da aplicação da estratégia de abstração de dados, interação com outras ferramentas (provadores de teoremas e verificadores de modelos) pode ser necessária. A ferramenta pode interagir com diferentes provadores de teoremas e verificadores de modelos, desde que o usuário altere suas configurações e implemente os plugins a serem utilizados. Na implementação disponível a ferramenta interage com o provador de teoremas Z-Eves.

6. Como conclusão, acreditamos que avançamos no estado-da-arte acerca da técnica de verificação de modelos aplicada a sistemas baseados em linguagens integradas bem como a sistemas infinitos. Partindo de um trabalho existente (que inclusive foi vencedor do CTD 2002), nosso trabalho representa um considerável avanço na teoria (teoremas comprovam as vantagens da nossa abordagem) e na parte prática com a ferramenta. Até o presente momento, não encontramos na literatura um trabalho que vise mecanizar a abstração de dados para linguagens integradas. A nossa ferramenta é um trabalho pioneiro no sentido de fornecer suporte à aplicação de uma técnica formal de gerar processos finitos usando abstração de dados. Uma prova desse reconhecimento é a aceitação de nosso trabalho para publicação em dois eventos internacionalmente reconhecidos: FME 2003 e IFM 2004.

De CSP_Z para CSP_M: uma Ferramenta Transformacional Java. Adalberto Farias and Alexandre Mota and Augusto Sampaio. In Proceedings of the IV Workshop on Formal Methods (WMF'2001), pages 1 - 10.

Comentário: Esse trabalho contribuiu com as primeiras idéias de mecanização da verificação de modelos na linguagem CSP_Z, concentrando-se mais especificamente na implementação da estratégia definida em [Mota e Sampaio 2001]. Uma vantagem comparando com a técnica definida para CSP-OZ em [Wehrheim and Fischer 1999] é a existência da ferramenta de suporte.

Efficient Analysis of Infinite CSP_Z Processes. Adalberto Farias and Alexandre Mota and Augusto Sampaio. In Proceedings of the V Workshop on Formal Methods (WMF'2002), pages 113 - 128.

Comentário: O trabalho refletiu a contribuição teórica para estratégia de abstração de dados. Nele foi proposto o algoritmo que também leva em consideração a parte de CSP quando abstraindo um processo CSP_Z. Este trabalho serviu de base para o artigo submetido à V conferência do IFM (Integrated Formal Methods).

A Support Tool for CSP_Z Data Abstraction. Adalberto Farias and Alexandre Mota and Augusto Sampaio. Tool Exibition Notes of the 12th International FME Symposium, pages 11 - 15.

Comentário: Esse trabalho representa a primeira contribuição prática da pesquisa, onde um primeiro protótipo foi apresentado num dos maiores eventos na área de Métodos Formais do mundo. O trabalho também é uma evidência de que a mecanização da técnica é possível e necessária para estimular o uso de Métodos Formais na indústria de software. O FME é um dos maiores eventos em métodos formais no mundo.

Efficient CSP_Z Data Abstraction. Adalberto Farias and Alexandre Mota and Augusto Sampaio. In Proceedings of IV International Conference on Integrated Formal Methods (IFM 2004), E. Boiten, J. Derrick, G. Smith editors. Lecture Notes in Computer Science, volume 2999, pages 108 - 127. Springer-Verlag, 2004.

Comentário: Esse trabalho é uma documentação da parte teórica (algoritmo) de prática (ferramenta) juntos num só trabalho, sendo que algumas melhorias e exemplos da aplicação da técnica foram mais explorados, como por exemplo, uma comparação com a técnica proposta em [Mota, Borba and Sampaio 2002] quando aplicada a processos cuja parte de Z é instável. O resultado é que o nosso algoritmo conseguiu produzir uma abstração para o processo porque a parte de CSP era estável. O evento IFM é também um evento fortemente reconhecido pela comunidade internacional de Métodos Formais.