Nesta seção, destacam-se as principais contribuições da tese, a saber, as ações voltadas a assegurar a correção do método BSmart, as ferramentas desenvolvidas, a biblioteca KitSmart e o estudo de caso do passaporte eletrônico.
Destaca-se que parte das especificações e demais artefatos produzidos na tese, bem como as ferramentas implementadas, podem ser obtidas no sítio http://code.google.com/p/bsmart/. Nesse endereço também encontram-se as instruções de instalação e execução das ferramentas de software.
9.1.1 Correção do Método BSmart
A tese enfatiza a correção do processo de desenvolvimento e geração de código com o método BSmart através de três abordagens principais, a saber:
I. Formalização e verificação do desenvolvimento (especificação e refinamentos) requerido pelo método BSmart utilizando o próprio método B e a ferramenta de verificação provida pelo Atelier B;
II. Especificação e verificação das bibliotecas do KitSmart;
III. Descrição das gramáticas das linguagens B0 e Java e o mapeamento da tradução entre cada elemento dessas linguagens através de regras de reescrita de termos em ASF+SDF.
Observa-se que a verificação do método assegura a correção do processo de especificação e refinamento e da adaptação de interface entre os componentes Java e Java Card. Esta parte da tese, apresentada no capítulo 4, utilizou-se de um desenvolvimento genérico em B, no qual, inicialmente, foram representados os elementos significativos da especificação relacionados à mudança de estado e à verificação. Esses elementos foram inseridos em máquinas de contexto na forma de constantes funcionais, contendo propriedades adicionais que definiam os aspectos a ser verificados para a sua correção, tal como a relação das entradas de uma operação com a sua pré-condição e, posteriormente, se a mudança de estado a partir desse novo valor respeita as restrições impostas pelo invariante. A partir desses componentes básicos foram então descritas e verificadas as máquinas e refinamentos componentes do método BSmart.
Ressalta-se que as bibliotecas do KitSmart também fornecem um auxílio ao processo de verificação do método, prevenindo a utilização incorreta dos componentes da API Java Card e possibilitando o uso adequado de tipos na especificação. É importante enfatizar os diversos componentes desta biblioteca que foram desenvolvidos ou aprimorados no decorrer desta tese. Dentre eles, destacam-se as máquinas de tipos básicos short, byte, int e boolean da linguagem Java, máquinas de biblioteca que podem ser utilizadas na implementação B para encapsular o estado de valores inteiros e sequências e os 93 componentes da biblioteca Java Card 2.2.2. Esse último ramo da biblioteca foi concluído no trabalho de mestrado de Simone Santos [San12]. Insta frisar que a biblioteca pode ser reutilizada em diversos projetos, mesmo sem vínculo com o método BSmart.
A especificação da tradução para Java Card em ASF+SDF, apesar de não se constituir em uma prova da tradução, fornece, potencialmente, uma maior confiança em sua correção, além de um elemento de documentação útil para a implementação das ferramentas, bem como
para futuros usuários e desenvolvedores. Ressalta-se que esse processo possibilita a verificação através da inspeção de cada elemento e da simulação da transformação entre as linguagens através da ferramenta Meta-Environment.
É importante enfatizar que o modelo em ASF+SDF não se configura em uma prova for- mal da tradução. Para tanto, seria necessário a descrição formal da semântica de ambas as linguagens e da transformação entre elas. Optou-se pela solução adotada ao se verificar que o tempo disponível para a realização desta tese, com o atendimento dos seus outros objetivos, não seria suficiente para concluir a tarefa de especificação semântica. Por outro lado, o trabalho desenvolvido pode servir como uma referência inicial para uma futura criação do seu modelo formal.
9.1.2 Suporte de Ferramentas ao Método
O suporte de ferramentas ao método BSmart foi outra importante contribuição da tese. Destaca-se o emprego da biblioteca BCompiler [Cle12b] ao desenvolvimento dos programas, fornecendo a verificação sintática e de tipos, assim como a geração da árvore de parser, a partir da qual torna-se possível acessar e manipular o código B. Outro benefício do uso dessa API foi compatibilizar o BSmart com a linguagem B fornecida para a ferramenta Atelier B.
Na tese, desenvolveu-se a biblioteca AMNPrinter que usa o BCompiler para possibilitar a geração de código de B para outro módulo B e para Java ou Java Card. Através desse componente, contribui-se com três programas, a saber, um gerador de aplicação host (host_gen), outro para automatizar a criação do refinamento full function e da sua máquina de contexto (ff_gen) e um tradutor de B para Java e JavaCard (b2java_gen).
Observa-se que o software pode ser executado em linha de comando ou ser integrado à interface gráfica fornecida pela ferramenta Atelier B. Deve-se preferir a segunda forma, tendo em vista tornar o desenvolvimento mais ágil e possibilitar o uso de toda a gama de ferramentas que o ambiente oferece.
9.1.3 Estudo de Caso
Cumpre salientar que o estudo de caso do passaporte eletrônico do capítulo 7 foi um im- portante auxílio à validação do método, da biblioteca KitSmart e do seu suporte de ferramentas. No primeiro caso, seguiu-se os passos delineados no método para especificar e verificar cor- retamente, até a implementação B, os métodos relacionados aos protocolos fundamentais do passaporte (Passive Authentication e Basic Access Control).
O estudo de caso possibilitou o teste e a melhoria das ferramentas, em especial o gera- dor de código, tendo em vista que boa parte da notação e das instruções para implementação B foram utilizadas. Para as demais ferramentas, que recebem como entrada uma máquina ou refinamento, também foram utilizadas dezenas de módulos B que possibilitaram testá-las com diversas combinações de elementos, tais como, substituições, predicados, expressões e as dife- rentes formas de definição de operações. A adoção da ferramenta em outros projetos também será importante para o seu aprimoramento e correção de eventuais erros.