Made available in DSpace on 2014-12-17T15:46:59Z (GMT). No. of bitstreams: 1
BrunoEGG_TESE.pdf: 2215931 bytes, checksum: 5d86c012a04f884e6dec73c92c1d88ef (MD5)
Previous issue date: 2012-06-01 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / Smart card applications represent a growing market. Usually this kind of application
manipulate and store critical information that requires some level of security, such as financial
or confidential information. The quality and trustworthiness of smart card software can
be improved through a rigorous development process that embraces formal techniques of
software engineering. In this work we propose the BSmart method, a specialization of the
B formal method dedicated to the development of smart card Java Card applications. The
method describes how a Java Card application can be generated from a B refinement process
of its formal abstract specification. The development is supported by a set of tools, which
automates the generation of some required refinements and the translation to Java Card client
(host) and server (applet) applications. With respect to verification, the method development
process was formalized and verified in the B method, using the Atelier B tool [Cle12a]. We
emphasize that the Java Card application is translated from the last stage of refinement, named
implementation. This translation process was specified in ASF+SDF [BKV08], describing the
grammar of both languages (SDF) and the code transformations through rewrite rules (ASF).
This specification was an important support during the translator development and contributes
to the tool documentation. We also emphasize the KitSmart library [Dut06, San12], an essential
component of BSmart, containing models of all 93 classes/interfaces of Java Card API 2:2:2,
of Java/Java Card data types and machines that can be useful for the specifier, but are not part
of the standard Java Card library. In other to validate the method, its tool support and the
KitSmart, we developed an electronic passport application following the BSmart method. We
believe that the results reached in this work contribute to Java Card development, allowing the
generation of complete (client and server components), and less subject to errors, Java Card
applications. / As aplica??es para smart cards representam um mercado que cresce a cada ano. Normalmente,
essas aplica??es manipulam e armazenam informa??es que requerem garantias
de seguran?a, tais como valores monet?rios ou informa??es confidenciais. A qualidade e a
seguran?a do software para cart?es inteligentes pode ser aprimorada atrav?s de um processo
de desenvolvimento rigoroso que empregue t?cnicas formais da engenharia de software. Neste
trabalho propomos o m?todo BSmart, uma especializa??o do m?todo formal B dedicada ao
desenvolvimento de aplica??es para smart cards na linguagem Java Card. O m?todo descreve,
em um conjunto de etapas, como uma aplica??o smart card pode ser gerada a partir de
refinamentos em sua especifica??o formal. O desenvolvimento ? suportado por um conjunto de
ferramentas, automatizando a gera??o de parte dos refinamentos e a tradu??o para as aplica??es
Java Card cliente (host) e servidora (applet). Ressalta-se que o processo de especifica??o e refinamento
descrito no m?todo foi formalizado e verificado utilizando o pr?prio m?todo B, com
o aux?lio da ferramenta Atelier B [Cle12a]. Destaca-se que a aplica??o Java Card ? traduzida a
partir do ?ltimo passo de refinamento, denominado de implementa??o. A especifica??o dessa
tradu??o foi feita na linguagem ASF+SDF [BKV08]. Inicialmente, descreveu-se as gram?ticas
das linguagens B e Java (SDF) e, em uma etapa posterior, especificou-se as transforma??es
de B para Java Card atrav?s de regras de reescrita de termos (ASF). Essa abordagem foi um
importante aux?lio durante o processo de tradu??o, al?m de servir ao prop?sito de document?lo.
Cumpre destacar a biblioteca KitSmart [Dut06, San12], componente essencial ao m?todo
BSmart, que inclui modelos em B de todas as 93 classes/interfaces da API Java Card na
vers?o 2:2:2, dos tipos de dados Java e Java Card e de m?quinas que podem ser ?teis ao
especificador, mas que n?o est?o presentes na API padr?o. Tendo em vista validar o m?todo,
seu conjunto de ferramentas e a biblioteca KitSmart, procedeu-se com o desenvolvimento, seguindo
o m?todo BSmart, de uma aplica??o de passaporte eletr?nico. Os resultados alcan?ados
neste trabalho contribuem para o desenvolvimento smart card, na medida em que possibilitam
a gera??o de aplica??es Java Card completas (cliente e servidor) e menos sujeitas a falhas.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufrn.br:123456789/17947 |
| Date | 01 June 2012 |
| Creators | Gomes, Bruno Emerson Gurgel |
| Contributors | CPF:00809085437, http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4768856U5, Moreira, Anamaria Martins, CPF:82573611787, http://lattes.cnpq.br/5861361541278876, Sampaio, Augusto Cezar Alves, CPF:41521633487, http://lattes.cnpq.br/3977760354511853, Oliveira, Marcel Vinicius Medeiros, CPF:02386943488, http://lattes.cnpq.br/1756952696097255, D?harbe, David Boris Paul |
| Publisher | Universidade Federal do Rio Grande do Norte, Programa de P?s-Gradua??o em Sistemas e Computa??o, UFRN, BR, Ci?ncia da Computa??o |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/doctoralThesis |
| Format | application/pdf |
| Source | reponame:Repositório Institucional da UFRN, instname:Universidade Federal do Rio Grande do Norte, instacron:UFRN |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0029 seconds