BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B

Java Card technology allows the development and execution of small applications embedded in smart cards. A Java Card application is composed of an external card client and of an application in the card that implements the services available to the client by means of an Application Programming Interface (API). Usually, these applications manipulate and store important information, such as cash and confidential data of their owners. Thus, it is necessary to adopt rigor on developing a smart card application to improve its quality and trustworthiness. The use of formal methods on the development of these applications is a way to reach these quality requirements. The B method is one of the many formal methods for system specification. The development in B starts with the functional specification of the system, continues with the application of some optional refinements to the specification and, from the last level of refinement, it is possible to generate code for some programming language. The B formalism has a good tool support and its application to Java Card is adequate since the specification and development of APIs is one of the major applications of B. The BSmart method proposed here aims to promote the rigorous development of Java Card applications up to the generation of its code, based on the refinement of its formal specification described in the B notation. This development is supported by the BSmart tool, that is composed of some programs that automate each stage of the method; and by a library of B modules and Java Card classes that model primitive types, essential Java Card API classes and reusable data structuresCoordenação de Aperfeiçoamento de Pessoal de Nível SuperiorA tecnologia Java Card permite o desenvolvimento e execução de pequenas aplicações embutidas em smart cards. Uma aplicação Java Card é composta por um cliente, externo ao cartão, e por uma aplicação contida no cartão que implementa os serviços disponíveis ao cliente por meio de uma Application Programming Interface (API). Usualmente, essas aplicações manipulam e armazenam informações importantes, tais como valores monetários ou dados confidenciais do seu portador. Sendo assim, faz-se necessário adotar um maior rigor no processo de desenvolvimento de uma aplicação smart card, visando melhorar a sua qualidade e confiabilidade. O emprego de métodos formais como parte desse processo é um meio de se alcançar esses requisitos de qualidade. O método formal B ´e um dentre os diversos métodos formais para a especificação de sistemas. O desenvolvimento em B tem início com a especificação funcional do sistema, continua com a aplicação opcional de refinamentos à especificação e, a partir do último nível de refinamento, é possível a geração de código para alguma linguagem de programação. O formalismo B conta com bom suporte de ferramentas e a sua aplicação a Java Card mostra-se bastante adequada, uma vez que a especificação e desenvolvimento de APIs ´e o ponto forte de B. O método BSmart aqui proposto visa promover o desenvolvimento rigoroso de aplicações Java Card a partir da geração de código da aplicação com base em refinamentos da sua especificação formal descrita na notação B. O processo de desenvolvimento descrito no método é apoiado pela ferramenta BSmart, a qual constitui-se por alguns programas que automatizam cada etapa do método; e por uma biblioteca de módulos B e classes Java Card que modelam tipos primitivos, classes essenciais da API Java Card e estruturas de dados reutilizávei