JCML - Java Card Modeling Language: Definição e Implementação

AUTOR(ES)
DATA DE PUBLICAÇÃO

2007

RESUMO

Métodos formais poderiam ser usados para especificar e verificar software on-card em aplicações Java Card. O estilo de programação para smart cards requer verificação em tempo de execução para condições de entrada em todos os métodos Java Card, onde o objetivo principal é preservar os dados do cartão. Projeto por Contrato, em particular, a linguagem JML, é uma opção para este tipo de desenvolvimento e verificação, pelo fato da verificação em tempo de execução ser parte da implementação pela JML. Contudo, JML e suas respectivas ferramentas para verificação em tempo de execução não foram projetadas com o foco nas limitações Java Card, sendo, dessa forma, não compatíveis com Java Card. Nesta dissertação, analisamos o quanto esta situação é realmente intrínseca às limitações Java Card e, se é possível re-definir a JML e suas ferramentas. Propomos requisitos para uma nova linguagem, a qual é compatível com Java Card e apresentamos como o compilador desta linguagem pode ser construído. JCML retira da JML aspectos não definidos em Java Card, como por exemplo, concorrência e tipos não suportados. Isto pode não ser o bastante, contudo, sem o esforço em otimização de código de verificação gerado pelo compilador, não é possível gerar código de verificação para rodar no cartão. O compilador JCML, apesar de ser bem mais restrito em relação ao compilador JML, está habilitado a gerar código de verificação compatível com Java Card, para algumas especificações lightweight. Como conclusão, apresentamos uma variante da JML compatível com Java Card, JCML (Java Card Modeling Language), com uma versão de seu compilador

ASSUNTO(S)

verificação runtime java card formal methods compiler jcml runtime verification jml jml métodos formais compilador java card sistemas de computacao jcml

ACESSO AO ARTIGO

Documentos Relacionados