3. Experiments
3.2. Experimental procedure
A plataforma Java Card vem recebendo bastante atenc¸˜ao por parte da comunidade acadˆemica e da ind´ustria. O mercado estrat´egico que estas aplicac¸˜oes representam, a neces- sidade de robustez e qualidade em seu desenvolvimento e as pr´oprias caracter´ısticas da plata- forma, como o fato de possuir uma m´aquina virtual Java com menos recursos e definir uma API bem mais restrita que a plataforma Java, fazem de Java Card um terreno f´ertil para pesquisas na ´area de m´etodos formais. Descreveremos algumas pesquisas que se concentram em torno da especificac¸˜ao de classes da API Java Card, de verificac¸˜oes em tempo de execuc¸˜ao, bem como
da aplicac¸˜ao automatizada de testes baseados em m´etodos formais para Java Card.
A especificac¸˜ao da API Java Card ´e uma ´area de aplicac¸˜ao de m´etodos formais a Java Card que vem recebendo bastante destaque. Uma vez que a implementac¸˜ao da API normalmente n˜ao ´e fornecida, de uma forma geral, o objetivo desses trabalhos ´e permitir que verificac¸˜oes sejam feitas nas classes Java Card que a utilizam, por meio da especificac¸˜ao formal da API. Em [MEI- JER; POLL, 2001] e [POLL; BERG; JACOBS, 2001] pode-se vislumbrar a especificac¸˜ao, por meio de anotac¸˜oes em Java Modelling Language (JML) [LEAVENS; CHEON, 2006], das clas- ses JCSystem e APDU, respectivamente. O trabalho de [LARSSON; MOSTOWSKI, 2004] fornece como estudo de caso a especificac¸˜ao da classe para autenticac¸˜ao OwnerPin em JML e
Object Constraint Language(OCL), fazendo uma comparac¸˜ao entre esses dois formalismos. Uma especificac¸˜ao em B do mecanismo de transac¸˜ao para Java Card foi feita em [SA- BATIER; LARTIGUE, 1999]. Essa especificac¸˜ao foi submetida a mais de 10 refinamentos, culminando com a sua implementac¸˜ao em B e, nesse processo, mais de 1500 obrigac¸˜oes de pro- vas foram corretamente verificadas. A partir da implementac¸˜ao B foi feita a gerac¸˜ao “manual” de c´odigo para a linguagem C.
A verificac¸˜ao do bytecode Java Card geralmente ´e efetuada fora do cart˜ao para assegurar que a aplicac¸˜ao a ser instalada segue a especificac¸˜ao Java Card e n˜ao compromete a seguranc¸a da m´aquina virtual ou de outros applets instalados no cart˜ao [ORT, 2001]. Em [CASSET; BURDY; REQUET, 2002], vem sendo desenvolvido um verificador de bytecode, gerado em linguagem C a partir da sua especificac¸˜ao em B, com otimizac¸˜oes de c´odigo e de utilizac¸˜ao de mem´oria, visando a sua instalac¸˜ao e execuc¸˜ao dentro do cart˜ao.
A gerac¸˜ao autom´atica de testes baseada em m´etodos formais para aplicac¸˜oes Java Card ´e tamb´em uma linha de pesquisa que vem recebendo alguma atenc¸˜ao, como pode ser visto por meio dos trabalhos de [WEELDEN et al., 2005] e [MARTIN; BOUSQUET, 2001].
Em [WEELDEN et al., 2005] foi feito um estudo sobre a aplicabilidade de testes caixa preta baseado em especificac¸˜oes formais em aplicac¸˜oes Java Card e fazer comparac¸˜oes com outras abordagens de teste para Java Card. Para a gerac¸˜ao dos dados, execuc¸˜ao e an´alise dos testes foi utilizada a ferramenta GAST [KOOPMAN ARTEM ALIMARINE; PLASMEIJER, 2002], que recebeu como entrada uma especificac¸˜ao com as propriedades do sistema como func¸˜oes na linguagem CLEAN2. A aplicac¸˜ao dos testes a um estudo de caso de carteira eletrˆonica foi feita de forma incremental. Uma pessoa ficou respons´avel por desenvolver a especificac¸˜ao da aplicac¸˜ao e outra a sua implementac¸˜ao. A cada interac¸˜ao, era aplicado o teste para verificar a conformidade da especificac¸˜ao com a implementac¸˜ao. Ao final do processo verificou-se que
essa abordagem era adequada, uma vez que conseguiu detectar as inconsistˆencias entre o mo- delo e a implementac¸˜ao final, tendo como resultado, segundo o autor, uma aplicac¸˜ao livre de erros.
No trabalho de Martin e Bousquet [MARTIN; BOUSQUET, 2001], que segue a mesma linha do trabalho anterior, inicialmente ´e feita a modelagem dos m´etodos do applet por meio de diagramas de estados UML. Estes s˜ao ent˜ao traduzidos, com o aux´ılio da ferramenta UM-
LAUT[HO; PENNANEAC’H; PLOUZEAU, 2000], em Labeled Transition Systems que servem como entrada para a ferramenta TGV [JARD; J ´ERON, 2005], que por sua vez gera os casos de teste. Os autores desenvolveram um pequeno programa para traduzir os casos de teste gerados em uma aplicac¸˜ao Java Card. Assim como no trabalho anterior, um estudo de caso de carteira eletrˆonica foi utilizado para a validac¸˜ao desta proposta. O programa gerado com base nos casos de teste inicializa as vari´aveis do applet e chama cada m´etodo, por meio de comandos APDU, passando diferentes parˆametros de teste. Por fim, as respostas de cada m´etodo s˜ao comparadas `as sa´ıdas esperadas para cada resposta. Na validac¸˜ao da proposta, um processo manual de teste de caixa-preta diretamente aplicado `a aplicac¸˜ao, ou seja, sem relac¸˜ao com o m´etodo proposto, foi feito e comparado com a proposta do artigo. De acordo com os autores, esta ´ultima mostrou- se superior, uma vez que conseguiu capturar todos os testes especificados no modelo abstrato, ao contr´ario da primeira.
Vimos alguns trabalhos de aplicac¸˜ao de m´etodos formais a Java Card preocupados com a especificac¸˜ao formal da sua API, outros com a verificac¸˜ao em tempo de execuc¸˜ao da aplicac¸˜ao
Java Carde, ainda, trabalhos que aplicam testes de caixa-preta com base em formalismos como aux´ılio `a validac¸˜ao da aplicac¸˜ao Java Card. O trabalho apresentado por esta dissertac¸˜ao n˜ao se enquadra em nenhum desses objetivos em particular. O foco deste trabalho, no momento, ´e o apoio ao desenvolvedor Java Card quanto ao desenvolvimento da aplicac¸˜ao do lado cart˜ao, tendo por base a gerac¸˜ao de c´odigo desta aplicac¸˜ao a partir da sua especificac¸˜ao formal em B.