Desenvolvimento formal de aplicações para Smart Cards /

Mostrar outras versões (1)

As aplicações para smart cards representam um mercado que cresce a cada ano. Nor-malmente, essas aplicações manipulam e armazenam informações que requerem garantias de segurança, tais como valores monetários ou informações conﬁdenciais. A qualidade e a segurança do software para cartões...

ver descrição completa

Na minha lista:

Detalhes bibliográficos
Principais autores:	Gomes, Bruno Emerson Gurgel., Déharbe, David Boris Paul., Universidade Federal do Rio Grande do Norte.
Formato:	Tese
Publicado em:
Assuntos:	Engenharia de software - Tese. Métodos formais - Método B - Java(Linguagem de programação de computador) - Ferramenta BSmart - Software for smart cards. BSmart method. Java Programming Language (computer).
Endereço do item:	https://repositorio.ufrn.br/jspui/bitstream/123456789/17947/1/BrunoEGG_TESE.pdf
Tags:	Adicionar Tag Sem tags, seja o primeiro a adicionar uma tag!

id	oai:localhost:123456789-121479
record_format	dspace
institution	Acervo SISBI
collection	SIGAA
topic	Engenharia de software - Tese. Métodos formais - Método B - Tese. Java(Linguagem de programação de computador) - Tese. Ferramenta BSmart - Tese. Software for smart cards. BSmart method. Java Programming Language (computer).
spellingShingle	Engenharia de software - Tese. Métodos formais - Método B - Tese. Java(Linguagem de programação de computador) - Tese. Ferramenta BSmart - Tese. Software for smart cards. BSmart method. Java Programming Language (computer). Gomes, Bruno Emerson Gurgel. Déharbe, David Boris Paul. Universidade Federal do Rio Grande do Norte. Desenvolvimento formal de aplicações para Smart Cards /
description	As aplicações para smart cards representam um mercado que cresce a cada ano. Nor-malmente, essas aplicações manipulam e armazenam informações que requerem garantias de segurança, tais como valores monetários ou informações conﬁdenciais. 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 reﬁnamentos em sua especiﬁcação formal. O desenvolvimento é suportado por um conjunto de ferramentas, automatizando a geração de parte dos reﬁnamentos e a tradução para as aplicações Java Card cliente (host) e servidora (applet). Ressalta-se que o processo de especiﬁcação e reﬁnamento descrito no método foi formalizado e veriﬁcado 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 reﬁnamento, denominado de implementação. A especiﬁcaçã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, especiﬁcou-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 especiﬁcador, 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, se-guindo 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.#$&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 ﬁnancial or conﬁdential 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 reﬁnement process of its formal abstract speciﬁcation. The development is supported by a set of tools, which automates the generation of some required reﬁnements and the translation to Java Card client (host) and server (applet) applications. With respect to veriﬁcation, the method development process was formalized and veriﬁed in the B method, using the Atelier B tool [Cle12a]. We emphasize that the Java Card application is translated from the last stage of reﬁnement, named implementation. This translation process was speciﬁed in ASF+SDF [BKV08], describing the grammar of both languages (SDF) and the code transformations through rewrite rules (ASF). This speciﬁcation 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 speciﬁer, 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.
format	Tese
author	Gomes, Bruno Emerson Gurgel. Déharbe, David Boris Paul. Universidade Federal do Rio Grande do Norte.
author_facet	Gomes, Bruno Emerson Gurgel. Déharbe, David Boris Paul. Universidade Federal do Rio Grande do Norte.
author_sort	Gomes, Bruno Emerson Gurgel.
title	Desenvolvimento formal de aplicações para Smart Cards /
title_short	Desenvolvimento formal de aplicações para Smart Cards /
title_full	Desenvolvimento formal de aplicações para Smart Cards /
title_fullStr	Desenvolvimento formal de aplicações para Smart Cards /
title_full_unstemmed	Desenvolvimento formal de aplicações para Smart Cards /
title_sort	desenvolvimento formal de aplicações para smart cards /
publishDate	2022
url	https://repositorio.ufrn.br/jspui/bitstream/123456789/17947/1/BrunoEGG_TESE.pdf
work_keys_str_mv	AT gomesbrunoemersongurgel desenvolvimentoformaldeaplicacoesparasmartcards AT deharbedavidborispaul desenvolvimentoformaldeaplicacoesparasmartcards AT universidadefederaldoriograndedonorte desenvolvimentoformaldeaplicacoesparasmartcards
_version_	1766810187302174720
spelling	oai:localhost:123456789-1214792022-11-30T22:16:26Z Desenvolvimento formal de aplicações para Smart Cards / Gomes, Bruno Emerson Gurgel. Déharbe, David Boris Paul. Universidade Federal do Rio Grande do Norte. Engenharia de software - Tese. Métodos formais - Método B - Tese. Java(Linguagem de programação de computador) - Tese. Ferramenta BSmart - Tese. Software for smart cards. BSmart method. Java Programming Language (computer). As aplicações para smart cards representam um mercado que cresce a cada ano. Nor-malmente, essas aplicações manipulam e armazenam informações que requerem garantias de segurança, tais como valores monetários ou informações conﬁdenciais. 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 reﬁnamentos em sua especiﬁcação formal. O desenvolvimento é suportado por um conjunto de ferramentas, automatizando a geração de parte dos reﬁnamentos e a tradução para as aplicações Java Card cliente (host) e servidora (applet). Ressalta-se que o processo de especiﬁcação e reﬁnamento descrito no método foi formalizado e veriﬁcado 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 reﬁnamento, denominado de implementação. A especiﬁcaçã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, especiﬁcou-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 especiﬁcador, 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, se-guindo 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.#$&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 ﬁnancial or conﬁdential 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 reﬁnement process of its formal abstract speciﬁcation. The development is supported by a set of tools, which automates the generation of some required reﬁnements and the translation to Java Card client (host) and server (applet) applications. With respect to veriﬁcation, the method development process was formalized and veriﬁed in the B method, using the Atelier B tool [Cle12a]. We emphasize that the Java Card application is translated from the last stage of reﬁnement, named implementation. This translation process was speciﬁed in ASF+SDF [BKV08], describing the grammar of both languages (SDF) and the code transformations through rewrite rules (ASF). This speciﬁcation 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 speciﬁer, 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. 1 2022-10-06T05:25:46Z 2022-10-06T05:25:46Z 2012. Tese 004.41 G633d TESE 185272 https://repositorio.ufrn.br/jspui/bitstream/123456789/17947/1/BrunoEGG_TESE.pdf https://repositorio.ufrn.br/jspui/bitstream/123456789/17947/1/BrunoEGG_TESE.pdf

Desenvolvimento formal de aplicações para Smart Cards /

Registros relacionados