| Summary: | Made available in DSpace on 2014-12-17T15:47:44Z (GMT). No. of bitstreams: 1
BrunoEGG.pdf: 1320681 bytes, checksum: 897ca75ef7f0e564e8588d949fcc67d5 (MD5)
Previous issue date: 2007-11-19 === Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior === 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 === 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
|
|---|
