Desenvolvimento de um Sistema de Automação e Supervisão de Máquinas Dispensadoras Através da Internet

This paper aims to design and develop a control and monitoring system of vending machines, based on a Central Processing Unit with peripheral Internet communication. Coupled with the condom vending machines, a data acquisition module will be connected to the original circuits in order to collect and send, via internet, the information to the healthy government agencies, in the form of charts and reports. In the face of this, such agencies may analyze these data and compare them with the rates of reduction, in medium or long term, of the STD/AIDS in their respective regions, after the implementation of these vending machines, together with the conventional preventing programs. Reading the methodology, this paper is about an explaining and bibliography research, with the aspect of a qualitative-quantitative methodology, presenting a deductive method of approach and an indirect documentation technique research. About the results of the tests and simulations, we concluded that the implementation of this system will have the same success in any other type of dispenser machine

JCML: A specification language for the runtime verification of Java Card programs

COSTA, Umberto Souza; MOREIRA, Anamaria Martins; MUSICANTE, Matin A.; SOUZA NETO, Plácido A. JCML: A specification language for the runtime verification of Java Card programs. Science of Computer Programming. [S.l]: [s.n], 2010.

Specification and Runtime Verification of Java Card Programs

COSTA, Umberto Souza da; MOREIRA, Anamaria Martins; MUSICANTE, Martin A. Specification and Runtime Verification of Java Card Programs. Electronic Notes in Theoretical Computer Science. [S.l:s.n], 2009.

Avaliação do desenvolvimento sustentável na bacia hidrográfica do Rio Seridó em face das políticas públicas e da gestão dos recursos hídricos

The reality of water resources management in semiarid regions, such as the Seridó region, has been shaped by a complex chain involving social-cultural, political, economic and environmental aspects, covering different spheres of activity - from local to federal. Because water is a scarce element, the most rational way pointed out by our recent history has been to move towards an increasing emphasis on the need for a truly rational, integrated, sustainable and participatory water resources management, supported by legislation and by a network of institutions that could materialize it. In this sense, despite all the advances in the formulation of public policies in water resources, which ones have indeed lead to significant changes that have occurred or are underway in semiarid regions such as Seridó? What factors may be preventing the realization of the desires rationality embedded in the framers of water policies intents? How to properly manage water resources if the current actors who promote their management and the political, human, cultural and institutional processes that intervene in this management, show strong traces of unsustainability? The research methodology adopted in this paper led to a breakdown of the traditional approach to water resource management, to integrate it into other areas of knowledge, especially to political science and public administration, catalyzed by the concept of "sustainable development". From a broad, interdisciplinary literature review, an exhaustive characterization of the river basin Seridó, a set of interviews with key people in the public administration acting in the region, a series of diagnoses and a set of propositions were made in order to correct the direction of current public policies for the region. From the point of view of public policies, it is in the deployment phase, not in its formulation, which lies a major problem of the lack of significant progress in water management. The lack of coordination between government programs are well characterized, as well as the lack of efficiency and effectiveness of their actions. The causes of this secular model are also discussed, including political factors and social relations of production, which led to a stalemate difficult, but of possible solution. It can be perceived there is a scenario of progressive deterioration of natural resources of the fragile ecosystem and a network of environmental and social consequences difficult to reverse, the result of a persistent and inertial sociopolitical culture, whose main factors reinforce itself. The work leads towards a characterization of the water resources management also from the perspective of environmental, institutional, political and human sustainability , the latter being identified, particularly as investment in the development of people as autonomous beings - not based in ideological directives of any kind - in the emancipation of the traditional figure of the poor man of the hinterland" to the "catalyst for change" responsible for their own decisions or omissions, based upon an education for free-thinking that brings each one as co-responsible epicenter of (self-) sustainable changes in their midst

Formal verification of PLC programs using the B Method

PLCs (acronym for Programmable Logic Controllers) perform control operations, receiving information from the environment, processing it and modifying this same environment according to the results produced. They are commonly used in industry in several applications, from mass transport to petroleum industry. As the complexity of these applications increase, and as various are safety critical, a necessity for ensuring that they are reliable arouses. Testing and simulation are the de-facto methods used in the industry to do so, but they can leave flaws undiscovered. Formal methods can provide more confidence in an application s safety, once they permit their mathematical verification. We make use of the B Method, which has been successfully applied in the formal verification of industrial systems, is supported by several tools and can handle decomposition, refinement, and verification of correctness according to the specification. The method we developed and present in this work automatically generates B models from PLC programs and verify them in terms of safety constraints, manually derived from the system requirements. The scope of our method is the PLC programming languages presented in the IEC 61131-3 standard, although we are also able to verify programs not fully compliant with the standard. Our approach aims to ease the integration of formal methods in the industry through the abbreviation of the effort to perform formal verification in PLCs