JCML - Java Card Modleing Language : definição e implementação/

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...

ver descrição completa

Na minha lista:

Detalhes bibliográficos
Principais autores:	Souza Neto, Plácido Antônio., Moreira, Anamaria Martins.
Formato:	Dissertação
Publicado em:
Assuntos:	Métodos formais - Dissertação. Java Card - Verificação runtime - Compilador - Formal methods. Java Card. Runtime verification. Compiler.
Endereço do item:	https://repositorio.ufrn.br/bitstream/123456789/17961/1/PlacidoASN.pdf
Tags:	Adicionar Tag Sem tags, seja o primeiro a adicionar uma tag!

id	oai:localhost:123456789-68935
record_format	dspace
spelling	oai:localhost:123456789-689352022-11-30T06:21:42Z JCML - Java Card Modleing Language : definição e implementação/ Souza Neto, Plácido Antônio. Moreira, Anamaria Martins. Métodos formais - Dissertação. Java Card - Dissertação. Verificação runtime - Dissertação. Compilador - Dissertação. Formal methods. Java Card. Runtime verification. Compiler. 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.#$&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. 1 2022-10-05T16:51:24Z 2022-10-05T16:51:24Z 2007. Dissertação 004.41 S729j DISSERT 97564 https://repositorio.ufrn.br/bitstream/123456789/17961/1/PlacidoASN.pdf https://repositorio.ufrn.br/bitstream/123456789/17961/1/PlacidoASN.pdf
institution	Acervo SISBI
collection	SIGAA
topic	Métodos formais - Dissertação. Java Card - Dissertação. Verificação runtime - Dissertação. Compilador - Dissertação. Formal methods. Java Card. Runtime verification. Compiler.
spellingShingle	Métodos formais - Dissertação. Java Card - Dissertação. Verificação runtime - Dissertação. Compilador - Dissertação. Formal methods. Java Card. Runtime verification. Compiler. Souza Neto, Plácido Antônio. Moreira, Anamaria Martins. JCML - Java Card Modleing Language : definição e implementação/
description	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.#$&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.
format	Dissertação
author	Souza Neto, Plácido Antônio. Moreira, Anamaria Martins.
author_facet	Souza Neto, Plácido Antônio. Moreira, Anamaria Martins.
author_sort	Souza Neto, Plácido Antônio.
title	JCML - Java Card Modleing Language : definição e implementação/
title_short	JCML - Java Card Modleing Language : definição e implementação/
title_full	JCML - Java Card Modleing Language : definição e implementação/
title_fullStr	JCML - Java Card Modleing Language : definição e implementação/
title_full_unstemmed	JCML - Java Card Modleing Language : definição e implementação/
title_sort	jcml - java card modleing language : definição e implementação/
publishDate	2022
url	https://repositorio.ufrn.br/bitstream/123456789/17961/1/PlacidoASN.pdf
work_keys_str_mv	AT souzanetoplacidoantonio jcmljavacardmodleinglanguagedefinicaoeimplementacao AT moreiraanamariamartins jcmljavacardmodleinglanguagedefinicaoeimplementacao
_version_	1766834364912500736

JCML - Java Card Modleing Language : definição e implementação/

Registros relacionados