Please use this identifier to cite or link to this item: https://repositorio.ufrn.br/handle/123456789/17961
Title: JCML - Java Card Modeling Language: Definição e Implementação
Authors: Souza Neto, Plácido Antônio de
Keywords: Métodos Formais;Java Card;JML;JCML;Verificação Runtime;Compilador;Formal Methods;Java Card;JML;JCML;Runtime Verification;Compiler
Issue Date: 6-Sep-2007
Publisher: Universidade Federal do Rio Grande do Norte
Citation: SOUZA NETO, Plácido Antônio de. JCML - Java Card Modeling Language: Definição e Implementação. 2007. 136 f. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal do Rio Grande do Norte, Natal, 2007.
Portuguese Abstract: 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
Abstract: Formal methods should be used to specify and verify on-card software in Java Card applications. Furthermore, Java Card programming style requires runtime verification of all input conditions for all on-card methods, where the main goal is to preserve the data in the card. Design by contract, and in particular, the JML language, are an option for this kind of development and verification, as runtime verification is part of the Design by contract method implemented by JML. However, JML and its currently available tools for runtime verification were not designed with Java Card limitations in mind and are not Java Card compliant. In this thesis, we analyze how much of this situation is really intrinsic of Java Card limitations and how much is just a matter of a complete re-design of JML and its tools. We propose the requirements for a new language which is Java Card compliant and indicate the lines on which a compiler for this language should be built. JCML strips from JML non-Java Card aspects such as concurrency and unsupported types. This would not be enough, however, without a great effort in optimization of the verification code generated by its compiler, as this verification code must run on the card. The JCML compiler, although being much more restricted than the one for JML, is able to generate Java Card compliant verification code for some lightweight specifications. As conclusion, we present a Java Card compliant variant of JML, JCML (Java Card Modeling Language), with a preliminary version of its compiler
URI: https://repositorio.ufrn.br/jspui/handle/123456789/17961
Appears in Collections:PPGSC - Mestrado em Sistemas e Computação

Files in This Item:
File Description SizeFormat 
PlacidoASN.pdf636.93 kBAdobe PDFThumbnail
View/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.