Desenvolvimento formal de aplicações para smartcards

Smart card applications represent a growing market. Usually this kind of application manipulate and store critical information that requires some level of security, such as financial or confidential information. The quality and trustworthiness of smart card software can be improved through a rigorous development process that embraces formal techniques of software engineering. In this work we propose the BSmart method, a specialization of the B formal method dedicated to the development of smart card Java Card applications. The method describes how a Java Card application can be generated from a B refinement process of its formal abstract specification. The development is supported by a set of tools, which automates the generation of some required refinements and the translation to Java Card client (host) and server (applet) applications. With respect to verification, the method development process was formalized and verified in the B method, using the Atelier B tool [Cle12a]. We emphasize that the Java Card application is translated from the last stage of refinement, named implementation. This translation process was specified in ASF+SDF [BKV08], describing the grammar of both languages (SDF) and the code transformations through rewrite rules (ASF). This specification was an important support during the translator development and contributes to the tool documentation. We also emphasize the KitSmart library [Dut06, San12], an essential component of BSmart, containing models of all 93 classes/interfaces of Java Card API 2:2:2, of Java/Java Card data types and machines that can be useful for the specifier, but are not part of the standard Java Card library. In other to validate the method, its tool support and the KitSmart, we developed an electronic passport application following the BSmart method. We believe that the results reached in this work contribute to Java Card development, allowing the generation of complete (client and server components), and less subject to errors, Java Card applications.

Tvoice :um sistema de manipulação de linguagens para auxiliar portadores de necessidades especiais através da web

This work presents the tVoice, software that manipulates tags languages, extracting information and, being integral part of the VoiceProxy system, it aids bearers of special needs in the access to the Web. This system is responsible for the search and treatment of the documents in the Web, extracting the textual information contained in those documents and preceding the capability of generating eventually through translation techniques, an audio script, used by the of interface subsystem of VoiceProxy, the iVoice, in the process of voice synthesis. In this stage the tVoice, besides the treatment of the tag language HTML, processes other two formats of documents, PDF and XHTML. Additionally to allow that, besides the iVoice, other interface subsystems can make use of the tVoice through remote access, we propose distribution systems techniques based in the model Client-Server providers operations of the fashion of a proxy server treatment of documents

Detecção e recuperação de falhas para a máquina de redução de grafos PEWS-AM

Web services are software units that allow access to one or more resources, supporting the deployment of business processes in the Web. They use well-defined interfaces, using web standard protocols, making possible the communication between entities implemented on different platforms. Due to these features, Web services can be integrated as services compositions to form more robust loose coupling applications. Web services are subject to failures, unwanted situations that may compromise the business process partially or completely. Failures can occur both in the design of compositions as in the execution of compositions. As a result, it is essential to create mechanisms to make the implementation of service compositions more robust and to treat failures. Specifically, we propose the support for fault recovery in service compositions described in PEWS language and executed on PEWS-AM, an graph reduction machine. To support recovery failure on PEWS-AM, we extend the PEWS language specification and adapted the rules of translation and reduction of graphs for this machine. These contributions were made both in the model of abstract machine as at the implementation level

Atores sociais e política ambiental urbana do Município de Mossoró/RN pelo prisma das cartografias sociais analíticas

It starts with the understanding that the relationship between society / nature is largely problematic in a context of socio-environmental crisis. In this context, we use the principle of hope to plan and work out new ways of understanding social reality, the relationship between science and alternative knowledge. The research is to investigate how the actors influence the social construction of urban environmental policy of the city of Mossoró / RN with reference to the processes of implementing the Master Plan and Agenda 21 of the municipality. The hypothesis of this research is that the Environmental Policy in Mossley has a normative character that is expressed primarily in the creation of an institutional political framework to manage environmental issues involving so incidental and or functional society participation mossoroense. Thus questioned who are the actors that build environmental policy Mossoró / RN. The specific objectives of this research are: Identify the environmental dimension of the Master Plan Agenda 21 articulated Mossoró / RN mapping information from the managers, engineers and members of the Municipal Environment and Municipal Council of Cities on the operation of urban environmental policy mossoroense and how it is performed by the Manager of Environmental Management in conjunction with the Department of Environment and Territorial Development (SEDETMA) and Executive Management of Urban Development. As a methodology, we used the method of the sociology of absences and emergencies in conjunction with the ecology of knowledge and productivity. It is a qualitative research and documentary, which was used as the Master Plan documents Mossoró / RN, minutes of meetings of boards and complementarity were carried out 12 semi-structured interviews with managers and directors of the Urban Environmental Policy of the Municipality of Mossoró / RN. They used also the social analytical or thematic maps for the translation of the dialogue among social partners, managers and directors who make the Environmental Policy Council. We conclude that these dialogues and experiences point to the construction of an environmental policy more participatory and effective, committed to individual and collective transformation of society mossoroense