Made available in DSpace on 2014-12-17T15:48:00Z (GMT). No. of bitstreams: 1 SimoneOS_DISSERT_capa_ate_pag44.pdf: 4276014 bytes, checksum: c178262769ab9981c0bbfc10faf1c633 (MD5) Previous issue date: 2012-02-10 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / 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 / 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

Made available in DSpace on 2014-12-17T15:47:56Z (GMT). No. of bitstreams: 1 DiegoHOS_DISSERT.pdf: 2899752 bytes, checksum: d3160b774efd6749eced9bb34d4a74cf (MD5) Previous issue date: 2011-08-31 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / Using formal methods, the developer can increase software s trustiness and correctness. Furthermore, the developer can concentrate in the functional requirements of the software. However, there are many resistance in adopting this software development approach. The main reason is the scarcity of adequate, easy to use, and useful tools. Developers typically write code and test it. These tests usually consist of executing the program and checking its output against its requirements. This, however, is not always an exhaustive discipline. On the other side, using formal methods one might be able to investigate the system s properties further. Unfortunately, specification languages do not always have tools like animators or simulators, and sometimes there are no friendly Graphical User Interfaces. On the other hand, specification languages usually have a compiler which normally generates a Labeled Transition System (LTS). This work proposes an application that provides graphical animation for formal specifications using the LTS as input. The application initially supports the languages B, CSP, and Z. However, using a LTS in a specified XML format, it is possible to animate further languages. Additionally, the tool provides traces visualization, the choices the user did, in a graphical tree. The intention is to improve the comprehension of a specification by providing information about errors and animating it, as the developers do for programming languages, such as Java and C++. / Usando m?todos formais, o desenvolvedor pode aumentar a confiabilidade e corretude do software. Al?m disso, o desenvolvedor pode concentrar-se mais nos requisitos funcionais. Por?m h? muita resist?ncia em se adotar essa abordagem de desenvolvimento de software. A raz?o principal e a escassez de suporte ferramental adequado, ?til e de f?cil utiliza??o. Os desenvolvedores normalmente escrevem o c?digo e o testam. Estes testes geralmente consistem em checar se as sa?das est?o de acordo com os requisitos. Isto, contudo, nem sempre e poss?vel de maneira exaustiva. Por outro lado, usando M?todos Formais um desenvolvedor e capaz de investigar profundamente as propriedades do sistema. Infelizmente, linguagens de especifica??o formal nem sempre possuem ferramentas como animador ou simulador e ?s vezes n?o h? interfaces gr?ficas amig?veis. Por?m, algumas dessas ferramentas possuem um compilador, que gera um Sistema de Transi??es Rotuladas (LTS). A proposta deste trabalho ? desenvolver um aplicativo que fornece anima??o gr?fica para especifica??es formais usando o LTS como entrada. O aplicativo inicialmente suporta as as linguagens B, CSP e Z. Usando o LTS em um formato XML especificado ? poss?vel animar outras linguagens formais. Adicionalmente a ferramenta disponibiliza visualiza??o de traces, escolhas feitas pelo usu?rio, em um formato de ?rvore gr?fica. A inten??o ? melhorar a compreens?o de uma especifica??o, fornecendo informa??es sobre erros e animando-a, como os desenvolvedores fazem com linguagens de programa??o como Java e C++.