Made available in DSpace on 2014-12-17T15:48:07Z (GMT). No. of bitstreams: 1 AntonioAOVS.pdf: 849695 bytes, checksum: 575cdb368ae14f3aad606763ebea7114 (MD5) Previous issue date: 2004-10-13 / The widespread growth in the use of smart cards (by banks, transport services, and cell phones, etc) has brought an important fact that must be addressed: the need of tools that can be used to verify such cards, so to guarantee the correctness of their software. As the vast majority of cards that are being developed nowadays use the JavaCard technology as they software layer, the use of the Java Modeling Language (JML) to specify their programs appear as a natural solution. JML is a formal language tailored to Java. It has been inspired by methodologies from Larch and Eiffel, and has been widely adopted as the de facto language when dealing with specification of any Java related program. Various tools that make use of JML have already been developed, covering a wide range of functionalities, such as run time and static checking. But the tools existent so far for static checking are not fully automated, and, those that are, do not offer an adequate level of soundness and completeness. Our objective is to contribute to a series of techniques, that can be used to accomplish a fully automated and confident verification of JavaCard applets. In this work we present the first steps to this. With the use of a software platform comprised by Krakatoa, Why and haRVey, we developed a set of techniques to reduce the size of the theory necessary to verify the specifications. Such techniques have yielded very good results, with gains of almost 100% in all tested cases, and has proved as a valuable technique to be used, not only in this, but in most real world problems related to automatic verification / O 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