KitSmart: Uma biblioteca de componentes para o desenvolvimento rigoroso de aplicações Java Card com o método B

Mostrar outras versões (1)

The development of smart card applications requires a high level of reliability. Formal methods provide means for this reliability to be achieved. The BSmart method and tool contribute to the development of smart card applications with the support of the B method, generating Java Card code from B s...

ver descrição completa

Na minha lista:
Detalhes bibliográficos
Autor principal: Santos, Simone de Oliveira
Outros Autores: Moreira, Anamaria Martins
Formato: Dissertação
Idioma:por
Publicado em: Universidade Federal do Rio Grande do Norte
Assuntos:
engenharia de Software
especificação formal
método B
java card
software engineering
formal specification
B method
CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO
Endereço do item:https://repositorio.ufrn.br/jspui/handle/123456789/18043
Tags: Adicionar Tag
Sem tags, seja o primeiro a adicionar uma tag!
id ri-123456789-18043
record_format dspace
institution Repositório Institucional
collection RI - UFRN
language por
topic engenharia de Software
especificação formal
método B
java card
software engineering
formal specification
B method
java card
CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO
spellingShingle engenharia de Software
especificação formal
método B
java card
software engineering
formal specification
B method
java card
CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO
Santos, Simone de Oliveira
KitSmart: Uma biblioteca de componentes para o desenvolvimento rigoroso de aplicações Java Card com o método B
description The development of smart card applications requires a high level of reliability. Formal methods provide means for this reliability to be achieved. The BSmart method and tool contribute to the development of smart card applications with the support of the B method, generating Java Card code from B specifications. For the development with BSmart to be effectively rigorous without overloading the user it is important to have a library of reusable components built in B. The goal of KitSmart is to provide this support. A first research about the composition of this library was a graduation work from Universidade Federal do Rio Grande do Norte, made by Thiago Dutra in 2006. This first version of the kit resulted in a specification of Java Card primitive types byte, short and boolean in B and the creation of reusable components for application development. This work provides an improvement of KitSmart with the addition of API Java Card specification made in B and a guide for the creation of new components. The API Java Card in B, besides being available to be used for development of applications, is also useful as a documentation of each API class. The reusable components correspond to modules to manipulate specific structures, such as date and time. These structures are not available for B or Java Card. These components for Java Card are generated from specifications formally verified in B. The guide contains quick reference on how to specify some structures and how some situations were adapted from object-orientation to the B Method. This work was evaluated through a case study made through the BSmart tool, that makes use of the KitSmart library. In this case study, it is possible to see the contribution of the components in a B specification. This kit should be useful for B method users and Java Card application developers
author2 Moreira, Anamaria Martins
author_facet Moreira, Anamaria Martins
Santos, Simone de Oliveira
format masterThesis
author Santos, Simone de Oliveira
author_sort Santos, Simone de Oliveira
title KitSmart: Uma biblioteca de componentes para o desenvolvimento rigoroso de aplicações Java Card com o método B
title_short KitSmart: Uma biblioteca de componentes para o desenvolvimento rigoroso de aplicações Java Card com o método B
title_full KitSmart: Uma biblioteca de componentes para o desenvolvimento rigoroso de aplicações Java Card com o método B
title_fullStr KitSmart: Uma biblioteca de componentes para o desenvolvimento rigoroso de aplicações Java Card com o método B
title_full_unstemmed KitSmart: Uma biblioteca de componentes para o desenvolvimento rigoroso de aplicações Java Card com o método B
title_sort kitsmart: uma biblioteca de componentes para o desenvolvimento rigoroso de aplicações java card com o método b
publisher Universidade Federal do Rio Grande do Norte
publishDate 2014
url https://repositorio.ufrn.br/jspui/handle/123456789/18043
work_keys_str_mv AT santossimonedeoliveira kitsmartumabibliotecadecomponentesparaodesenvolvimentorigorosodeaplicacoesjavacardcomometodob
_version_ 1773962165693186048
spelling ri-123456789-180432017-11-04T15:15:43Z KitSmart: Uma biblioteca de componentes para o desenvolvimento rigoroso de aplicações Java Card com o método B Santos, Simone de Oliveira Moreira, Anamaria Martins http://lattes.cnpq.br/5922034090094531 http://lattes.cnpq.br/5861361541278876 Déharbe, David Boris Paul http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4768856U5 Gheyi, Rohit http://lattes.cnpq.br/2931270888717344 engenharia de Software especificação formal método B java card software engineering formal specification B method java card CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO The development of smart card applications requires a high level of reliability. Formal methods provide means for this reliability to be achieved. The BSmart method and tool contribute to the development of smart card applications with the support of the B method, generating Java Card code from B specifications. For the development with BSmart to be effectively rigorous without overloading the user it is important to have a library of reusable components built in B. The goal of KitSmart is to provide this support. A first research about the composition of this library was a graduation work from Universidade Federal do Rio Grande do Norte, made by Thiago Dutra in 2006. This first version of the kit resulted in a specification of Java Card primitive types byte, short and boolean in B and the creation of reusable components for application development. This work provides an improvement of KitSmart with the addition of API Java Card specification made in B and a guide for the creation of new components. The API Java Card in B, besides being available to be used for development of applications, is also useful as a documentation of each API class. The reusable components correspond to modules to manipulate specific structures, such as date and time. These structures are not available for B or Java Card. These components for Java Card are generated from specifications formally verified in B. The guide contains quick reference on how to specify some structures and how some situations were adapted from object-orientation to the B Method. This work was evaluated through a case study made through the BSmart tool, that makes use of the KitSmart library. In this case study, it is possible to see the contribution of the components in a B specification. This kit should be useful for B method users and Java Card application developers Coordenação de Aperfeiçoamento de Pessoal de Nível Superior O desenvolvimento de aplicações para smart cards requer um alto grau de confiabilidade. Métodos formais fornecem meios para que esta confiabilidade seja alcançada. O método e a ferramenta BSmart fornecem uma contribuição para que o desenvolvimento para smart cards seja feito com o auxílio do método formal B, gerando código Java Card a partir de especificações B. Para que o desenvolvimento com o BSmart seja efetivamente rigoroso sem sobrecarregar o usuário do método é importante que haja uma biblioteca de componentes reutilizáveis feitos em B. O KitSmart tem como objetivo prover esse auxílio. Um primeiro estudo sobre a composição dessa biblioteca foi tema de uma monografia de graduação do curso de Bacharelado em Ciência da Computação da Universidade Federal do Rio Grande do Norte, feita por Thiago Dutra em 2006. Esta primeira versão do kit resultou na especificação dos tipos primitivos permitidos em Java Card (byte, short e boolean) em B e a criação de componentes reutilizáveis para o desenvolvimento de aplicações. Esta dissertação provê o aperfeiçoamento do KitSmart com o acréscimo da especificação da API Java Card em B, e um guia para o desenvolvimento de novos componentes. A API Java Card especificada em B, além de estar disponível para ser usada no desenvolvimento de projetos, serve como documentação ao especificar restrições de uso para cada classe da API. Os componentes reutilizáveis correspondem a módulos para manipulação de estruturas específicas, como data e hora, por exemplo. Estes tipos de estruturas não estão disponíveis em B ou Java Card. Os componentes reutilizáveis para Java Card são gerados a partir das especificações verificadas formalmente em B. O guia contém informações de consulta rápida para especificação de diversas estruturas e como algumas situações foram contornadas para adaptar a orientação a objetos ao Método B. Este trabalho foi avaliado através de um estudo de caso feito com a ferramenta BSmart que faz uso da biblioteca KitSmart. Neste estudo de caso, é possível ver a contribuição dos componentes em uma especificação B. Este kit deverá ser útil tanto para usuários do método B como para desenvolvedores de aplicações Java Card em geral 2014-12-17T15:48:00Z 2012-09-20 2014-12-17T15:48:00Z 2012-02-10 masterThesis SANTOS, Simone de Oliveira. KitSmart: Uma biblioteca de componentes para o desenvolvimento rigoroso de aplicações Java Card com o método B. 2012. 97 f. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal do Rio Grande do Norte, Natal, 2012. https://repositorio.ufrn.br/jspui/handle/123456789/18043 por Acesso Aberto application/pdf application/pdf Universidade Federal do Rio Grande do Norte BR UFRN Programa de Pós-Graduação em Sistemas e Computação Ciência da Computação

Registros relacionados