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 structures

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

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

Recanto do vale do pium: condomínio de habitações com ênfase no baixo impacto ambiental e no desempenho térmico do ambiente construído

This work describes the design process of a small recreational gated community in Pium, Nísia Floresta/RN, from concept to final design stages, with emphasis on low environmental impact, thermal comfort and the spatial quality of housing. The process consisted in a review of the literature and relevant standards, studies of design references and architectural programming. The project development was initially focused on the project’s feasibility, with the definition of the number of units, implantation, size and location of the dwellings and the common areas of the development. Two types of houses (four low rise and five duplex units) have been proposed in order to attend the premises of architectural programming. The conception of the architectural design began with the rooms’ zoning according to the lots. This resulted in the pre-selection of three alternatives that were evaluated in terms of spatial quality and environmental performance. The development of sketches focused on the envelope consistent with the bioclimatic guidelines and on the language of the compatible proposal with the lowest possible environmental impact of the building system, which resulted in the selection of the eucalyptus wood type. During the working drawings, the Quality Technical Regulation for the Level of Energy Efficiency Residential Buildings (RTQ -R) was adopted for the evaluation of the envelope, which resulted in "B" level of efficiency for the first case. After minor adjustments, mainly in frames, the efficiency level rose to "A", demonstrating that early project decisions contributed to the envelope energy performance. Besides the design of the two types of units, the final proposal of the gated community includes the design of the equipment for the common areas (entrance, multipurpose room and support and service sector), and the descriptive texts explaining the project and construction’s details.