Navegando por Autor "Silva, Antonio Augusto Viana da"
Agora exibindo 1 - 1 de 1
- Resultados por página
- Opções de Ordenação
Dissertação Contribuições para verificação automática de applets javacard(Universidade Federal do Rio Grande do Norte, 2004-10-13) Silva, Antonio Augusto Viana da; Déharbe, David Boris Paul; ; http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4768856U5; ; http://lattes.cnpq.br/3769079916577408; Silva, Ivan Saraiva; ; http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4780113E2; Perkusich, Angelo; ; http://lattes.cnpq.br/9439858291700830O grande crescimento do uso de smart cards (por bancos, companhias de transporte, celulares, etc) trouxe um fato importante, que deve ser considerado: a necessidade de ferramentas que possam ser usadas para verificar os cartões, para que se possa garantir a corretude de seu software. Como a grande maioria dos cartões desenvolvidos hoje em dia usa a tecnologia JavaCard em sua camada de software, o uso da Java Modeling Language (JML) para especificar os programas aparece como uma solu¸ao natural. JML é uma linguagem de especificação formal ligada ao Java. Ela foi inspirada pelas metodologias de Larch e Eiffel, e foi largamente adotada como a linguagem de facto em se tratando da especificação de qualquer programa relacionado à Java. Várias ferramentas que fazem uso de JML já foram desenvolvidas, cobrindo uma grande gama de funcionalidades, entre elas, a verificação em tempo de execução e estática. Mas as ferramentas existentes até o momento para a verificação estática não são totalmente automatizadas, e, aquelas que são, não oferecem um nível adequado de completude e segurança. Nosso objetivo é contribuir com uma série de técnicas, que podem ser usadas para alcançar uma verificação completamente automática e segura para applets JavaCard. Nesse trabalho nós apresentamos os primeiros passos nessa direção. Com o uso de uma plataforma de software composta pelo Krakatoa, Why e haRVey, nós desenvolvemos um conjunto de técnicas para reduzir o tamanho da teoria necessária para verificar as especificações. Tais técnicas deram resultados muito bons, com ganhos de quase 100% em todos os testes que realizamos, e se provou como uma técnica que deve ser sempre considerAda, não somente nesse, mas na maioria dos problemas reais relacionado com verificação automática