A presente seção descreve algumas ferramentas de suporte ao desenvolvimento formal de software. Ela foi propositalmente inserida antes das demais devido às ferramentas ora apre- sentadas serem utilizadas por diversos trabalhos que são descritos nas próximas seções. Será detalhado de forma geral o propósito de cada ferramenta e as suas principais funcionalidades. Nas demais seções, os aspectos específicos de cada uma delas podem ser revisitados, como, por exemplo, a sua utilização para a geração de código.
A ferramenta JBtools [Voi02] foi uma das primeiras abordagens acadêmicas a prover um gerador de código da linguagem B para linguagens orientadas a objetos. No caso, as linguagens- alvo escolhidas para a tradução foram Java e C# e, até certo ponto, conforme discutir-se-á posteriormente, Java Card. Além de geração de código, o ambiente de desenvolvimento JBtools fornece verificação de tipos em uma especificação B, geração de documentação em HTML e uma biblioteca para a manipulação de um módulo B, denominada de B Object Library BOL.
É interessante detalhar o componente BOL, devido à sua utilização na versão inicial da ferramenta BSmart. A BOL contém uma classe para cada elemento da especificação B. Após a verificação de tipos bem-sucedida em uma especificação, é gerado um arquivo XML contendo a representação de cada elemento de notação do módulo que foi verificado como uma marcação XML. Essas marcações são lidas e proporcionam a montagem de uma árvore de objetos da BOL. A partir desses objetos é então possível a fácil manipulação de um módulo B para diversas tarefas, tais como análise do código, geração de um novo módulo B ou refinamento e tradução. Ressalta-se também a plataforma de desenvolvimento Brillant [MC10], uma iniciativa de código aberto para suporte e experimentação com o método formal B. O conjunto de software
definido pelo Brillant inclui parser, verificador de tipos, tradutor de código e um gerador de obrigações de prova. O gerador ainda não está completo, mas implementa a maior parte das construções e propriedades de prova descritas no B-Book [Abr96]. As obrigações de prova vêm sendo geradas em um formato compatível com o provador de teoremas Coq [INR10]. De forma similar ao que é feito para o JBtools, para permitir a integração das diversas ferramentas, um formato intermediário em XML do desenvolvimento é gerado.
O Atelier B [Cle12a] é uma importante ferramenta de suporte ao método B, sendo utilizada em diversos projetos na indústria e na academia. O Atelier B fornece um conjunto de ferra- mentas integradas a uma IDE, dentre as quais destaca-se um verificador de tipos, um gerador de obrigações de prova e um provador que fornece a verificação das obrigações de prova de forma automatizada ou com assistência do usuário (interativa), essa última deve ser utilizada quando determinada obrigação de prova não consegue ser verificada de forma automática.
Cumpre observar que além das ferramentas mencionadas, o Atelier B, na sua versão mais recente (4.1), inclui a ferramenta Bart e um gerador de código de B para C, denominado de ComenC [Cle12c]. O software Bart possibilita a geração automatizada de refinamentos em uma especificação ou refinamento B até a sua implementação. Inicialmente, deve-se especifi- car o padrão de refinamento desejado para as variáveis, a inicialização e as substituições das operações do módulo alvo do refinamento. Essa especificação é feita por meio de regras de refinamento e submetida ao Bart, que tenta casar o padrão estabelecido nas regras com as cons- truções do módulo a ser refinado. Sempre que um padrão é estabelecido, a regra de refinamento associada é aplicada, resultando, ao final do processo, na implementação concreta do módulo refinado. Observa-se que os refinamentos obtidos devem ser verificados, assim como qualquer outro refinamento, usando as obrigações de prova padrão de B.
No que concerne a animação de uma especificação B, que pode ser entendido como o processo de simulação da “execução” da especificação para fins de teste, destacam-se as fer- ramentas ProB [LBBP10] e Brama [Ser07]. A ferramenta ProB permite, além da animação, a verificação de modelos em uma especificação B ou Z. Em suas primeiras versões, ela utilizava a biblioteca BOL provida pelo JBtools. Nas versões mais recentes do ProB, essa biblioteca foi substituída por um parser e verificador de tipos B desenvolvidos pelos seus próprios autores. Por sua vez, o software Brama é desenvolvido pela Clearsy, a empresa que fornece a ferramenta Atelier B. Brama permite a construção de um modelo visual em Flash que conecta-se ao módulo de animação da especificação, permitindo assim a execução de uma especificação de maneira visualmente mais atrativa.
O projeto Deploy (anteriormente Rodin)1tem por objetivo a criação de técnicas e ferramen-
tas para o desenvolvimento de sistemas complexos de software, integrando métodos formais a técnicas de desenvolvimento de sistemas tolerantes a falhas. O projeto vem sendo desenvol- vido por grandes centros de ensino e pesquisa europeus, como Instituto Federal de Tecnologia (ETH) de Zurique e a Universidade de Southampton, em parceria com empresas privadas, como a Bosch, Siemens e a Space Systems Finland, que fornecem estudos de caso de sistemas de grande porte e testam as técnicas e ferramentas propostas no projeto. Atualmente, a ferramenta Rodin, que vem sendo desenvolvida no âmbito deste projeto, é a implementação de referência para o formalismo Event-B [Abr10].
A ferramenta Rodin é composta por um kernel básico, distribuído como um plugin para a plataforma Eclipse, e que serve de base para a integração de diversos plugins com ferramentas específicas para suporte à metodologia, dentre os quais, destacam-se o plugin para o desenvol- vimento básico com Event-B e outro que inclui o gerador de obrigações de prova e o provador da ferramenta Atelier B. Ferramentas externas também podem ser integradas ao ambiente, tais quais o ProB, Brama e o software UML-B, que permite a tradução de diagramas em uma nota- ção similar à UML para especificações na linguagem B e Event-B. O Rodin é uma plataforma aberta e extensível que vem sendo continuamente aprimorada e atualizada com novos plugins. A versão estável atual do Rodin pode ser obtida no sítio http://www.event-b.org/install.html.
Ressalte-se que a ferramenta BSmart, desenvolvida no presente trabalho, não se propõe, a princípio, a ser tão abrangente quanto o plugin Rodin ou, ainda, a ferramenta Atelier B. O con- junto de software oferecido pelo BSmart visa apoiar o desenvolvimento formal de aplicações smart cards, seguindo o método formal B. Para tanto, o básico de serviços de suporte ao de- senvolvimento em B é oferecido, como a verificação de tipos e de obrigações de prova através da integração com as ferramentas do Atelier B e Batcave [MdMJD+08]. Na versão inicial, o
processo com o Atelier B em linha de comando era iniciado e posteriormente acessado dentro do ambiente do BSmart, na plataforma Eclipse. Atualmente, a integração tornou-se ainda mais forte, com as ferramentas do BSmart podendo ser incorporadas ao ambiente gráfico do Ate- lier Batravés do seu mecanismo de extensão. Além disso, as ferramentas utilizam o software BCompiler [Cle12b], o mesmo utilizado pelo Atelier B e seus programas, para possibilitar a manipulação de um módulo B e a geração de código.
Observa-se que, com o uso do BCompiler, conseguiu-se uma solução estável para a verifi- cação de tipos e a manipulação da especificação, com a vantagem de alinhar o desenvolvimento com a linguagem B do Atelier B. Conforme delineado na seção 4.6, as ferramentas fornecidas
pelo BSmart compreendem um gerador de refinamento full function, um gerador para a apli- cação host a partir da especificação inicial e o tradutor da implementação B para Java e Java Card. Essa última também verifica se a implementação satisfaz as restrições observadas para uma classe Java Card.