Banca de DEFESA: SIMONE DE OLIVEIRA SANTOS

Uma banca de DEFESA de MESTRADO foi cadastrada pelo programa.
DISCENTE: SIMONE DE OLIVEIRA SANTOS
DATA: 10/02/2012
HORA: 10:00
LOCAL: Sala de reuniões do DIMAp
TÍTULO:

KitSmart: Uma biblioteca de componentes para o desenvolvimento rigoroso de aplicações Java Card com o método B.

PALAVRAS-CHAVES:

Smart cards, Métodos Formais, Java Card, Biblioteca de componentes

PÁGINAS: 100
GRANDE ÁREA: Ciências Exatas e da Terra
ÁREA: Ciência da Computação
RESUMO:

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 booleano) e a idéia da criação de módulos adicionais 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, módulos reutilizáveis para desenvolvimento 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 módulos reutilizáveis correspondem a componentes 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 módulos adicionais 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 kit deverá ser útil tanto para usuários do método B como para desenvolvedores de aplicações Java Card em geral.

MEMBROS DA BANCA:
Presidente - 1258224 - ANAMARIA MARTINS MOREIRA
Interno - 2220777 - DAVID BORIS PAUL DEHARBE
Externo à Instituição - ROHIT GHEYI - UFCG