BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B

Mostrar outras versões (1)

Java Card technology allows the development and execution of small applications embedded in smart cards. A Java Card application is composed of an external card client and of an application in the card that implements the services available to the client by means of an Application Programming Interf...

ver descrição completa

Na minha lista:
Detalhes bibliográficos
Autor principal: Gomes, Bruno Emerson Gurgel
Outros Autores: Moreira, Anamaria Martins
Formato: Dissertação
Idioma:por
Publicado em: Universidade Federal do Rio Grande do Norte
Assuntos:
Java Card
Métodos formais
Método B
Geração de código.
Formal methods,
B method
Code generation
CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO
Endereço do item:https://repositorio.ufrn.br/jspui/handle/123456789/17964
Tags: Adicionar Tag
Sem tags, seja o primeiro a adicionar uma tag!
id ri-123456789-17964
record_format dspace
institution Repositório Institucional
collection RI - UFRN
language por
topic Java Card
Métodos formais
Método B
Geração de código.
Java Card
Formal methods,
B method
Code generation
CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO
spellingShingle Java Card
Métodos formais
Método B
Geração de código.
Java Card
Formal methods,
B method
Code generation
CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO
Gomes, Bruno Emerson Gurgel
BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B
description Java Card technology allows the development and execution of small applications embedded in smart cards. A Java Card application is composed of an external card client and of an application in the card that implements the services available to the client by means of an Application Programming Interface (API). Usually, these applications manipulate and store important information, such as cash and confidential data of their owners. Thus, it is necessary to adopt rigor on developing a smart card application to improve its quality and trustworthiness. The use of formal methods on the development of these applications is a way to reach these quality requirements. The B method is one of the many formal methods for system specification. The development in B starts with the functional specification of the system, continues with the application of some optional refinements to the specification and, from the last level of refinement, it is possible to generate code for some programming language. The B formalism has a good tool support and its application to Java Card is adequate since the specification and development of APIs is one of the major applications of B. The BSmart method proposed here aims to promote the rigorous development of Java Card applications up to the generation of its code, based on the refinement of its formal specification described in the B notation. This development is supported by the BSmart tool, that is composed of some programs that automate each stage of the method; and by a library of B modules and Java Card classes that model primitive types, essential Java Card API classes and reusable data structures
author2 Moreira, Anamaria Martins
author_facet Moreira, Anamaria Martins
Gomes, Bruno Emerson Gurgel
format masterThesis
author Gomes, Bruno Emerson Gurgel
author_sort Gomes, Bruno Emerson Gurgel
title BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B
title_short BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B
title_full BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B
title_fullStr BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B
title_full_unstemmed BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B
title_sort bsmart: desenvolvimento rigoroso de aplicações java card com base no método formal b
publisher Universidade Federal do Rio Grande do Norte
publishDate 2014
url https://repositorio.ufrn.br/jspui/handle/123456789/17964
work_keys_str_mv AT gomesbrunoemersongurgel bsmartdesenvolvimentorigorosodeaplicacoesjavacardcombasenometodoformalb
_version_ 1773966748138078208
spelling ri-123456789-179642017-11-04T13:22:56Z BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B Gomes, Bruno Emerson Gurgel Moreira, Anamaria Martins http://lattes.cnpq.br/7812661521592212 http://lattes.cnpq.br/5861361541278876 Déharbe, David Boris Paul http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4768856U5 Oliveira, Marcel Vinicius Medeiros http://lattes.cnpq.br/1756952696097255 Java Card Métodos formais Método B Geração de código. Java Card Formal methods, B method Code generation CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO Java Card technology allows the development and execution of small applications embedded in smart cards. A Java Card application is composed of an external card client and of an application in the card that implements the services available to the client by means of an Application Programming Interface (API). Usually, these applications manipulate and store important information, such as cash and confidential data of their owners. Thus, it is necessary to adopt rigor on developing a smart card application to improve its quality and trustworthiness. The use of formal methods on the development of these applications is a way to reach these quality requirements. The B method is one of the many formal methods for system specification. The development in B starts with the functional specification of the system, continues with the application of some optional refinements to the specification and, from the last level of refinement, it is possible to generate code for some programming language. The B formalism has a good tool support and its application to Java Card is adequate since the specification and development of APIs is one of the major applications of B. The BSmart method proposed here aims to promote the rigorous development of Java Card applications up to the generation of its code, based on the refinement of its formal specification described in the B notation. This development is supported by the BSmart tool, that is composed of some programs that automate each stage of the method; and by a library of B modules and Java Card classes that model primitive types, essential Java Card API classes and reusable data structures Coordenação de Aperfeiçoamento de Pessoal de Nível Superior A tecnologia Java Card permite o desenvolvimento e execução de pequenas aplicações embutidas em smart cards. Uma aplicação Java Card é composta por um cliente, externo ao cartão, e por uma aplicação contida no cartão que implementa os serviços disponíveis ao cliente por meio de uma Application Programming Interface (API). Usualmente, essas aplicações manipulam e armazenam informações importantes, tais como valores monetários ou dados confidenciais do seu portador. Sendo assim, faz-se necessário adotar um maior rigor no processo de desenvolvimento de uma aplicação smart card, visando melhorar a sua qualidade e confiabilidade. O emprego de métodos formais como parte desse processo é um meio de se alcançar esses requisitos de qualidade. O método formal B ´e um dentre os diversos métodos formais para a especificação de sistemas. O desenvolvimento em B tem início com a especificação funcional do sistema, continua com a aplicação opcional de refinamentos à especificação e, a partir do último nível de refinamento, é possível a geração de código para alguma linguagem de programação. O formalismo B conta com bom suporte de ferramentas e a sua aplicação a Java Card mostra-se bastante adequada, uma vez que a especificação e desenvolvimento de APIs ´e o ponto forte de B. O método BSmart aqui proposto visa promover o desenvolvimento rigoroso de aplicações Java Card a partir da geração de código da aplicação com base em refinamentos da sua especificação formal descrita na notação B. O processo de desenvolvimento descrito no método é apoiado pela ferramenta BSmart, a qual constitui-se por alguns programas que automatizam cada etapa do método; e por uma biblioteca de módulos B e classes Java Card que modelam tipos primitivos, classes essenciais da API Java Card e estruturas de dados reutilizáveis 2014-12-17T15:47:44Z 2008-02-26 2014-12-17T15:47:44Z 2007-11-19 masterThesis GOMES, Bruno Emerson Gurgel. BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B. 2007. 119 f. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal do Rio Grande do Norte, Natal, 2007. https://repositorio.ufrn.br/jspui/handle/123456789/17964 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