1 |
KitSmart: Uma biblioteca de componentes para o desenvolvimento rigoroso de aplica??es Java Card com o m?todo BSantos, Simone de Oliveira 10 February 2012 (has links)
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
|
2 |
Joker: um realizador de desenhos animados para linguagens formaisSouza, Diego Henrique Oliveira de 31 August 2011 (has links)
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++.
|
Page generated in 0.0821 seconds