Desenvolvimento Formal de Aplicações para Smart Cards
Smart Cards, Java Card, Métodos Formais, Método B,
Refinamento, Desenvolvimento Formal, Geração de Código
As aplicações para smart cards representam um mercado
que cresce a cada ano. Normalmente, essas aplicações
manipulam e armazenam informações que requerem garantias de
segurança, tais como valores monetários ou informações confidenciais.
A qualidade e a segurança do software smart card pode ser aprimorada
através de um processo de desenvolvimento rigoroso que empregue técnicas
formais da engenharia de software. Neste trabalho propomos o
método BSmart, uma especialização do método formal B dedicada
ao desenvolvimento de aplicações para smart cards
na linguagem Java Card. O método descreve, em um conjunto de etapas,
como uma aplicação smart card pode ser gerada a partir de
refinamentos em sua especificação formal. O trabalho a ser desenvolvido
é um aprimoramento da dissertação de mestrado do autor desta proposta.
No trabalho anterior, o foco maior foi o desenvolvimento inicial do método
e das ferramentas essenciais para o desenvolvimento e geração de
código de B para Java Card. No entanto, a verificação do processo de
desenvolvimento e geração de código não foi tratada. O trabalho proposto
na tese prioriza a formalização e a verificação de todo processo de
refinamento descrito no método e das etapas de geração de
código da aplicação Java Card. Também faz parte da contribuição
da tese a geração da aplicação cliente Java Card e
o tratamento formal da sua comunicação com a aplicação que reside no
cartão, denominada de applet. Dessa forma, o trabalho proposto
pretende contribuir de forma relevante ao desenvolvimento
para smart cards, possibilitando a geração de aplicações
Java Card completas (cliente e servidor), seguras e
menos sujeitas a falhas.