A verificação da relação de refinamento entre o modelo abstrato Passport e o seu correspon- dente concreto Passport_JC é feita em conformidade com a abordagem de adaptação descrita no capítulo 4 (seção 4.4). A ideia básica consiste em demonstrar que, mesmo possuindo inter- face distinta da máquina abstrata Passport, o modelo concreto equivale a um refinamento dessa. As obrigações de prova geradas para este refinamento foram corretamente verificadas com o auxílio do provador da ferramenta Atelier B.
O refinamento Passport_ref da máquina Passport, referencia o módulo Applet, que por sua vez contém a instância da máquina Passport_JC concreta. O invariante de Passport_ref estabelece a relação de refinamento entre o estado abstrato e o correspondente concreto através da instância na máquina Applet (perState = applet.perState ∧ ...).
Com relação às operações, a abordagem de refinamento consiste em conciliar a incompati- bilidade entre as interfaces, ao traduzir os parâmetros abstratos nos correspondentes concretos,
REFINEMENT Passport_ref REFINES Passport
SEES JByte, JShort, JBoolean, ISO7816,Apdu_Properties,
Passport_Context, Passport_JC_FF_Context, FileSystem_Context, InterfaceContext INCLUDES fileSystem.FileSystem, applet.Applet
INVARIANT perState = applet.perState ∧ volState = applet.volState ∧ selectedFile = applet.selectedFile ∧ rnd = applet.rnd ∧ ssc = applet.ssc INITIALISATION skip
Figura 7.21: Refinamento Passport_ref, máquinas inclusas e invariante.
tais como os campos p1, p2 e o array data_in, fornecidos à operação processAPDU. A partir do código de instrução (campo ins), a operação processAPDU irá requisitar o serviço concreto correspondente. O serviço é então realizado sob os dados fornecidos, alterando as variáveis de estado e o estado global da aplicação, de modo equivalente ao realizado na operação abstrata. Após a execução do serviço, os dados recebidos em data_out são retornados e convertidos para o tipo correspondente na saída abstrata.
Observa-se que a compatibilidade de tipos na conversão/decodificação dos dados é verifi- cada por meio de funções inseridas na máquina InterfaceContext (fig. 7.22), vista pelo com- ponente abstrato, pelo modelo Applet e pelo componente concreto, quando necessário. Cada função é definida em par, uma que converte e a outra que realiza a operação contrária. Por exemplo, a função seq_of_byte recebe um byte e indica a inserção desse byte em uma sequên- cia. Por sua vez, byte_of_seq, realiza a operação contrária, indicando a conversão de um byte a partir de uma uma posição na sequência.
MACHINE InterfaceContext
SEES JByte, JShort, JBoolean, FileSystem_Context CONCRETE_CONSTANTS
seq_of_byte, byte_of_seq, seq_of_short, short_of_seq, boolean_of_byte, byte_of_boolean
PROPERTIES
seq_of_byte∈ JBYTE 7→ seq1(JBYTE) ∧ seq_of_byte= λ (v1).(v1 ∈ JBYTE | [v1]) ∧ byte_of_seq∈ seq1(JBYTE) 7→ JBYTE ∧
byte_of_seq= λ (v1).(v1 ∈ seq1(JBYTE) ∧ size(v1) ≥ 1 ∧ v1(1) ∈ JBYTE | v1(1)) ∧ seq_of_short∈ JSHORT 7→ seq1(JBYTE) ∧
short_of_seq∈ seq1(JBYTE) 7→ JSHORT ∧
short_of_seq−1= seq_of_short ∧
boolean_of_byte∈ JBYTE 7→ JBOOLEAN ∧
boolean_of_byte= {1 7→ TRUE} ∧
boolean_of_byte= {0 7→ FALSE} ∧
byte_of_boolean∈ JBOOLEAN 7→ JBYTE ∧
byte_of_boolean= {TRUE 7→ 1} ∧
byte_of_boolean= {FALSE 7→ 0} END
Como exemplo, na figura 7.23, tem-se o refinamento da operação abstrata processGetChal- lenge. A conversão do parâmetro protectedAPDU em um byte, sendo esse enviado no campo p1, é feita com o auxílio da função byte_of_boolean (p1 := byte_of_boolean (protectedAPDU)). Por sua vez, o trecho de código data := seq_of_short(le) representa a conversão de le, um va- lor short, na sequência data. O retorno de processAPDU corresponde ao número randômico gerado, que por ser uma sequência de bytes, não necessita de conversão ao ser recebido pela variável de saída rnd_val.
rnd_val← processGetChallenge (protectedAPDU, le) = VAR
apdu, cla, ins, p1, p2, lc, data, data_out IN apdu:∈ APDU; cla:= CLA_NUMBER; ins:= processGetChallenge_INS; p1 := byte_of_boolean (protectedAPDU); p2 := cast_byte (0); lc := cast_byte (2); data:= seq_of_short(le); SELECT size (data) ≥ 1 ∧ size (data) ≤ 127 THEN
data_out← applet.processAPDU(apdu, cla, ins, p1, p2, lc, data, cast_byte(8)); rnd_val:= data_out
END END;
Figura 7.23: Operação refinada processGetChallenge.
7.9 Considerações Finais
Inicialmente, é importante enfatizar que o desenvolvimento do estudo de caso do passa- porte eletrônico possibilitou a validação e o aprimoramento do método BSmart, dos módulos do KitSmart utilizados, bem como de todo o suporte ferramental ao método. Apesar de, na ver- são atual, não se tratar de um desenvolvimento de grande complexidade ou de nível industrial, ele exercita boa parte da notação B de cláusulas, substituições e expressões.
Em relação ao método, o estudo de caso motivou a decisão de separar o módulo applet do módulo desenvolvimento principal dos serviços Java Card. Caso não fosse feito dessa forma, teríamos os métodos do applet inseridos diretamente no desenvolvimento, o que criaria uma distorção em relação à máquina abstrata, uma vez que a implementação concreta teria mais serviços que o modelo abstrato, o que não é permitido para o refinamento no B clássico. Além disso, os serviços do próprio módulo Passport_JC não poderiam ser requisitados dentro dos métodos do applet (process e install, por exemplo) caso eles fizessem parte de Passport_JC .
durante o desenvolvimento do estudo de caso. Modificou-se os tipos de dados, por exemplo, de array (função total) para sequência de byte, tendo em vista facilitar as obrigações de prova. Assim como pré-condições e implementação dos modelos de tipos de dados básicos e das clas- ses da API utilizadas foram corrigidos. Observa-se, ainda, que nem todas as classes foram exercitadas, o que deve ser feito como trabalho futuro através de outros estudos de caso.
A utilização da especificação Passport na validação da tradução também foi de suma im- portância, uma vez que no módulo de tradução, muito da notação B, dos tipos de dados e da composição de máquinas pôde ser verificado. Algumas diretrizes de como proceder com a im- plementação e decisões de projeto também foram estabelecidas, e são detalhadas no capítulo 5 que descreve a tradução do refinamento concreto B para Java Card. O desenvolvimento foi traduzido em classes Java Card e realizou-se a verificação sintática para o Java 1.3 através da IDE Eclipse. A efetiva instalação e teste da aplicação em um cartão (ou simulador) ainda não foi realizada, sendo objeto de trabalho futuro.
É importante destacar o esforço de prova no desenvolvimento do passaporte seguindo o método BSmart. No total, foram geradas 1155 obrigações de prova, em maior número nas implementações B, sendo 255 de Passport_JC_imp, 160 de Applet_i e 137 do refinamento Pas- sport_ref. No estudo de caso, é possível realizar a maior parte da verificação com o provador automático da ferramenta Atelier B. Por outro lado, ao utilizar o provador interativo, percebeu- se um ganho significativo no tempo de prova, ao se aplicar os comandos adequados de forma manual. Sendo assim, preferiu-se utilizar esse último modo de prova durante a maior parte do desenvolvimento. Além disso, com o uso do modo interativo, verificou-se que certos padrões de prova se repetiam. Nesse caso, uma melhoria a ser feita é a criação de táticas de prova que auxiliem o provador a aplicar diretamente os passos de verificação para esses casos.
Como trabalhos futuros pretende-se, na especificação cartão, realizar o desenvolvimento dos demais serviços que são necessários aos protocolos AA e EAC. Em relação ao cliente, espera-se identificar um subconjunto dessa parte da aplicação que poderia ser inserido, moti- vando a geração do cliente a partir da sua implementação B, e não apenas com base na interface das operações do modelo abstrato, como é feito atualmente.