Please use this identifier to cite or link to this item: https://repositorio.ufrn.br/jspui/handle/123456789/17964
Title: BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B
Authors: Gomes, Bruno Emerson Gurgel
Keywords: Java Card;Métodos formais;Método B;Geração de código.;Java Card;Formal methods,;B method;Code generation
Issue Date: 19-Nov-2007
Publisher: Universidade Federal do Rio Grande do Norte
Citation: 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.
Portuguese Abstract: 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
Abstract: 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
URI: http://repositorio.ufrn.br:8080/jspui/handle/123456789/17964
Appears in Collections:PPGSC - Mestrado em Sistemas e Computação

Files in This Item:
File Description SizeFormat 
BrunoEGG.pdf1.29 MBAdobe PDFThumbnail
View/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.