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

Cloud Integrator: uma plataforma para composição de serviços em ambientes de computação em nuvem

With the advance of the Cloud Computing paradigm, a single service offered by a cloud platform may not be enough to meet all the application requirements. To fulfill such requirements, it may be necessary, instead of a single service, a composition of services that aggregates services provided by different cloud platforms. In order to generate aggregated value for the user, this composition of services provided by several Cloud Computing platforms requires a solution in terms of platforms integration, which encompasses the manipulation of a wide number of noninteroperable APIs and protocols from different platform vendors. In this scenario, this work presents Cloud Integrator, a middleware platform for composing services provided by different Cloud Computing platforms. Besides providing an environment that facilitates the development and execution of applications that use such services, Cloud Integrator works as a mediator by providing mechanisms for building applications through composition and selection of semantic Web services that take into account metadata about the services, such as QoS (Quality of Service), prices, etc. Moreover, the proposed middleware platform provides an adaptation mechanism that can be triggered in case of failure or quality degradation of one or more services used by the running application in order to ensure its quality and availability. In this work, through a case study that consists of an application that use services provided by different cloud platforms, Cloud Integrator is evaluated in terms of the efficiency of the performed service composition, selection and adaptation processes, as well as the potential of using this middleware in heterogeneous computational clouds scenarios

Contribuições para verificação automática de applets javacard

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

Competitividade de destinos turísticos e o imperativo sustentável: avaliação de dimensões e atributos condicionantes no Pólo Costa das Dunas, RN, Brasil

Being available as a tourist destination is a necessary condition but not enough for the expansion and success of tourism activity. To be successful, tourism requires investment, inputs, appropriate planning and management, like any other economic activity. A fundamental goal of the destination management is to understand how the competitiveness of a tourist destination can be improved and sustained. Competitive position of tourism can be measured and assessed by various models. Evaluating the indicators of competitiveness of a tourist destination involves a multivariate analysis, ranging from issues directly related to tourism activity itself to the indirect factors. These are elements that are interrelated and that together will point out the competitive condition of this destination. From the definition and characterization of competitiveness, sustainability and management in the context of tourist destinations, understood as the main concepts of this study, we present the main theoretical and methodological models of assessment of competitiveness of tourist destinations in the literature and represent the state of the issue in the scientific treatment of the subject. These models, designed by researchers from several countries and applied in different tourist destinations, are confronted about their structure, indicators considered and localities in which they were applied. The aim of this study was to know and evaluate the condition of tourist competitiveness of the destination Pólo Costa das Dunas, from the constraints attributes of superior performance of the evaluation model of tourist competitiveness of destinations Competenible, suggested by Mazaro, and that suit the requirements of international market aware of the strength and importance of sustainability. The condition of competitiveness of tourist destination in Rio Grande do Norte Pólo Costa das Dunas was moderate. The competitive strengths and weaknesses of the destination Pólo Costa das Dunas revealed through the dozens of sustainable attributes of the model Competenible showed guidelines and initiatives that can be taken to guide strategic decisions related to their planning and management. Thus, this study should serve as support for strategic planning and long-term management of the sector and as a crucial tool for making decisions related to public policies, sectoral investments, monitor processes, strategic planning, direction and control of the local and regional tourism development of destinations

O Turismo como um tema de pesquisa: um diálogo epistemológico a partir das produções dos programas de pós-graduação stricto sensu da Universidade Federal do Rio Grande do Norte, no período de 2007 a 2011

The study consists in an analysis of researches with tourism issues, in Master s and Doctoral level, investigating their epistemological trends, regarding the type of study that is being produced and the methods used. It is characterized as exploratory, documental and bibliographical, having undertaken a cross-sectional study which covers the period from 2007 to 2011. It analyzes the context of academically production in tourism, the nature of these researches, the methodological aspects adopted in these theses and dissertations, the philosophical inclinations and the coherence and contribution of the same. This research uses, the Digital Library of Theses and Dissertations (BDTD) and the secretariats of the Academic Centers of the Federal University of Rio Grande do Norte (UFRN) as means to collect data. It employs the technique of sampling by judgment and undertakes the research in various Academic Centers in UFRN, using the method of content analysis. It shows that, from the 643 studies analyzed, 43 of them have themes related to tourism, which characterized this study sample. This study realizes that PPGA is the largest producer of researches on tourism issues, ahead of PPGTur, which ranks the third position, in this aspect. Also realizes that all surveys analyzed are crosssectional and the theme further investigated, with 21% of the sample, is related to the marketing aspects of tourism, with the theme Directors of Hotels and Restaurants (DHR) . This research demonstrates that all sample surveys make use of interviews, and these are, mostly, structured. Also realizes that most of these studies, with 21% of the sample, employ the method of content analysis. The references in Portuguese are surveyed about five times more than the ones in other languages. It estimates that more than half of the sample is characterized as positivist, associated with aspects of functionalism. A minority of 21% of these researches seeks to identify and recommend solutions to the tourism issues, or even represent part of them. This research concludes that the studies in tourism are mostly unifocal, being driven by issues related to the touristic trade. PPGTur produces a number still unrepresentative of studies. The theses and dissertations of the sample are limited and/or unable to analyze the changes of the phenomenon caused by the time. The studies from the sample present criteria and make use of other methods and techniques to associate with the interviews and content analysis to obtain more solid and reliable data and results. They use a low number of references in languages other than Portuguese. Most of these studies, characterized as positivist-functionalist, investigate the functioning, planning, coordination and expectations in organizations, leaving aside other issues, also relevant for tourism. The number of studies aimed at identifying solutions to the problems of tourism, or that even represents part of them, is not expressive

Análise da percepção da qualidade ambiental e de serviços turísticos em João Pessoa/PB

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior

Entendendo as interações entre povos pesqueiros, manguezal e área protegida: RDS estadual Ponta do Tubarão (RN, Brasil)

The mangrove ecosystem has a great importance to maintaining marine biodiversity, and to the livelihoods of communities living around it. Despite its importance, many mangrove areas have been extensively cleared and converted to other uses. There are few places where communities can retain their traditional uses of mangrove. A good example of conservation of traditional costumes are the fishing communities of the Sustainable Development Reserve (Reserva de Desenvolvimento Sustentável RDS) Ponta do Tubarão. The creation of the reserve came from the own population, and the devastation of a mangrove area, which would be destined for activity shrimp, was one of the reasons that led the population to ask authorities the establishment of a legally protected area. Thus, this study aimed to investigate the environmental perception of the fishing communities of RDS Ponta do Tubarão with respect to the mangroves in a biological, ecological and social perspective as well as evaluate the influence of the reserve in the mangrove conservation and quality of life. To meet objectives of this study was required the appropriation of some method and approaches of ethnosciences and environmental perception. Data were collected through direct observation, and semi-structured interviews. Through content analysis found that the population has a strong dependence on the mangrove ecosystem, as well as provides a good ecological knowledge of ecosystem functions. It was also found that the reservation has a good performance in the conservation of the mangroves; however, need to outline strategies to conciliate both the biological and cultural conservation.

ENTENDENDO AS INTERAÇÕES ENTRE POVOS PESQUEIROS, MANGUEZAL E ÁREA PROTEGIDA: RDS ESTADUAL PONTA DO TUBARÃO (RN, BRASIL)

The mangrove ecosystem has a great importance to maintaining marine biodiversity, and to the livelihoods of communities living around it. Despite its importance, many mangrove areas have been extensively cleared and converted to other uses. There are few places where communities can retain their traditional uses of mangrove. A good example of conservation of traditional costumes are the fishing communities of the Sustainable Development Reserve (Reserva de Desenvolvimento Sustentável RDS) Ponta do Tubarão. The creation of the reserve came from the own population, and the devastation of a mangrove area, which would be destined for activity shrimp, was one of the reasons that led the population to ask authorities the establishment of a legally protected area. Thus, this study aimed to investigate the environmental perception of the fishing communities of RDS Ponta do Tubarão with respect to the mangroves in a biological, ecological and social perspective as well as evaluate the influence of the reserve in the mangrove conservation and quality of life. To meet objectives of this study was required the appropriation of some method and approaches of ethnosciences and environmental perception. Data were collected through direct observation, and semi-structured interviews. Through content analysis found that the population has a strong dependence on the mangrove ecosystem, as well as provides a good ecological knowledge of ecosystem functions. It was also found that the reservation has a good performance in the conservation of the mangroves; however, need to outline strategies to conciliate both the biological and cultural conservation.

Zoneamento geoambiental como subsídio ao planejamento territorial municipal: estudo de caso para Currais Novos/RN

This paper presents the master plan and geoenvironmental zoning natures as instruments of environmental planning and management. The discussion of territory environmental planning is guided by two directions: at first the environmental elements involved in planning and the another is the implementation of these instruments at the municipal territory. To analyze the planning directed of the municipal territory we consider the fragments of its, represented by country and urban. The master plan inside of the Estatuto da Cidade (City Statute) and the geoenvironmental zoning are directed to territorial environmental planning. Regarding of the master plan the first challenge has been the spacial area that the plan can cover. It is necessary to prepare master plans that could include all the territory. The environmental zoning are directed for the territory totality.In this sense, the geoenvironmental zoning of the Currais Novos was done in the totality of the municipal territory and guided by the environmental physics variables. The geoenvironmental zoning sets in a planning and ordering of the territory instrument based in the landscape analysis. Therefore grounded in the Geosystems‟s Theory this work has like a main objective to propose a geoenvironmental zoning for the Currais Novos Municipality in RN. So, was used an analysis technique suggested for Bardin (2010) and the Currais Novos‟s physical environment characterization through of the fieldwork and cartographic data vectorization, beyond the image‟s treatment SRTM. The geoenvironmental systems definitions were based in the suggestion of Cestaro, et al. (2007) support in Bertrand (1968). For both were identified five geoenvironmental systems: Borborema Plateau, Residual plateau, Chapada da Serra de Santana, semiarid river valley and lagoon valley and eleven geoenvironmental subsystems: Borborema Plateau Western Slope, Isolated Massif of the Borborema Plateau, Residual Crest, Residual Massif, Erosional Scarp of the Chapada, flat top plateau, fluvial plains, temporary river of the semiarid and ornamental water or sluice

A contribuição da asstênia técnica no desenvolvimento desenvolvimento de projetos de assentamento no estado do Rio Grande do Norte

The public policies must have as their aimed the primordial at improving quality of life of families of a given population, however, its performance must be constantly monitored and evaluated scoped to ascertain whether these policies are reaching those goals. This work consisted in search of bibliographies and analysis that addressed the historical evolution of the debate on the subject of agrarian reform in Brazil as public policy and on the policy of technical assistance and rural extension, and collecting data in loco, in order to assess whether the actions implemented under this latter contribute to improvements in local development of settlements projects (PA) land reform in the state of Rio Grande do Norte (RN), this given the constant presented criticisms regarding their effectiveness, considering that it is difficult to empirically differentiate settlements they received of those who did not receive the technical assistance services. In this way, was held the data collection for comparison of characteristics (social organization, relationship with the local environment, form of producing and evaluation of technical assistance services) of two settlements in RN, being one you have received the technical assistance services and another who has not had access to these services in the past five years, at least, to confirm whether those who had access to the above services presents best features of social organization and the relationship with the local environment, mainly, which was confirmed in the results obtained, which still demonstrated that no significant differences on the forma to produce and of commercialization in PA studied. It was also found that the problems faced by families settled in PA studied resemble those seen verified in many other Brazilian states, especially as to how to use natural resources in the areas of land reform and the instability of the availability of technical assistance services. Should be guaranteed at continuity and universality of technical assistance services to settlements, seeking a higher focus on productive issues, which provide the income necessary for families settled can have a better quality of life

Triagem antifúngica de extratos obtidos de espécies vegetais do nordeste brasileiro

The increase in the incidence of fungal infections due to the drug-resistance or to the number of patients with immune alterations such as AIDS, chemotherapy or organ transplantation, has done the research necesseray for new antifungal drugs. The species from Northeastern Brazil may become an important source of innovative natural molecules. To evaluate the antifungal activity of 10 medicinal plants from Northeastern Brazil, traditionally used as antimicrobial agents, 30 crude extracts (CE) were tested in vitro against four standard species of Candida spp. The CE most promising of these plants were evaluated against yeasts of the oral cavity of kidney transplant patients and through a bioassay-guided fractionation. The extracts form leaves of E. uniflora, the stem bark of L. ferrea and leaves of P. guajava showed significant activity against all yeasts evaluated, with MIC values between 15.62 and 62.5 μg/mL. E. uniflora also showed fungicidal properties against all yeasts, especially against Candida dubliniensis. In patients with immune systems compromised, such as transplanted, oral candidiasis manifests mainly due to immunosuppressive therapy, and resistance to conventional antifungals. The CE of E. uniflora presented range of MIC values between 1.95 to 1000 μg/mL, and lower MIC50 and MIC90 values were observed against C. non-albicans. Due the better results, the CE of E. uniflora was elected to performe the bioassay-guided fractionation. Thus it was possible to obtain enriched fractions, which showed good inhibitory ability against ATCC strains of Candida spp. It was also possible to perform experiments to verify the production of biofilm in two strains of C. dubliniensis and action of extracts and fractions on the same. With this, we observed a behavior between the yeast ATCC and clinical isolate. In addition, CE, fractions and subfractions of E. uniflora inhibit planktonic cells to preventing the growth of biofilm. The preliminary chemical characterization of the fractions obtained revealed the presence of polyphenols (especially flavonoids and tannins). Finally, the results suggests that among the plant species studied, E. uniflora showed a pattern very promising as regards the antifungal, requiring further study of purification and structural elucidation of compounds in order to verify that the antifungal effect found can be attributed to a specific compound or some mechanism depends on synergistic the mixture of polyphenols

Projeto político de formação do enfermeiro: contextos, textos, (re)construções

This research analyses politic Project for nursing education, in its articulation with economical, political and social context of 1970s and 1980s in national level and, in special, nurse formation process in FAEN/UERN space, situating it on the context of Brazilian sanitary reformation movement and participation movement. The thesis is firmed on the sense of explaining whether that movement circa the nurse formation process has been able to build necessary instruments for the transformation of biomedical formation model historically consolidated, in the perspective of conceiving another model anchored on social determination of health/illness process, with the purpose of assuring ethical and political commitment with the SUS praised by sanitary reformation. The study visualized the object considering its specificity, its concrete historical determinations and institutional as well as organizational relationships that permeate possibilities of valorizing it, analyzing it, interpreting it and rebuilding it. Its operationalization occurred in three movements, it means, bibliographical review; documents study; interviews and focal groups realized with professors of the institution. We can apprehend as main results that the nurse formation process has incorporated widely spread conceptions by the sanitary reformation movement and participation movement, assuming the commitment with transformation of health services and social reality. Nevertheless it prevails, still, amongst some professors in the same institutional space, the commitment to a predominantly technicist formation, focused on instrumental knowledge. Opinion divergence explicit diversity of conceptions circa education and, as consequence, distinct political commitments, also contradictory to formation. Thus, there is a lacuna between what is foreseen on political pedagogical project and what is rendered in FAEN/UERN, evidencing the clash related to conceptual bases of formation project. Interpretations, divergent political attitudes and resistances to the process allowed several formation ways. However, formation under new conceptual bases, find limits on the context of social politics implemented in Brazil during the 1990s, neoliberal-based, expressed on expansion and consolidation of health private system, managed by market rules, strengthening biomedical formation model. Notwithstanding, there is a favorable to its implementation, starting from the first years of 21st century, moment when Brazilian sanitary reformation reappear on health speech, as well as facing the policy of permanent education in health. This reality explicit a process of dialectical tension between instituted and institutor, anticipating the moment of scission or adaptation and return to what is already known. Despite of clashed, knowledge, accumulated experience, contribution to services, the construction of partnerships out of university space and articulation with national movement of (re)orientation of nurse formation, have been constituted as vital instruments to offer support to formation in FAEN/UERN. Still, we consider necessary the (re)visitation to FAEN/UERN politic pedagogical Project considering the existing and implemented construction, without, yet, depreciate the norther axis of the project at the reaching of its intentionality

A temática ambiental na educação superior : políticas, gestão acadêmica e projetos de formação nos cursos da Universidade do Estado do Rio Grande do Norte

Conselho Nacional de Desenvolvimento Científico e Tecnológico

Democratização do acesso a água no semi-árido: o caso da comunidade rural de Pendências dos Emídios no município de Serrinha/RN

Brazil lives a time of experimentation and maturity as it pertains to managing the use of water, which comes institutionalising increasingly social participation. In Rio Grande do Norte, since 1997, the government has been developing actions accordingly, through the State Department of Water Resources, which has implemented a programme of adutoras within the State and created Water Users Associations, in the installation of dessalinizadores for places where the Adutora was not necessary or not yet arrived, so that should be managed by communities through associations of users. Since 2003, Civil Society Organisations - CSOs come through ASA - Articulation in the Semi-arid Brazilian, implementing the P1MC - Program of Training and Mobilization for Social Living with the Semi-Arid (One Million Rural Cisternas), in its third year of implementation in Rio Grande do Norte, in the spirit of working together with the semi arid. In the municipality of Serrinha / RN which incorporates the Semi-arid region, we find in the rural community of Pendêcias dos Emídios the experience of the State and Civil Society, which referred to a discussion about the environmental sustainability of these initiatives. The general objective of this work is to examine the strategies for participatory management in the use and access to water in the community of Pendêcias dos Emídios of the municipality of Serrinha / RN, to understand how those experiences can contribute to environmental sustainability. The methodology used envolvel bibliographic research in categories involving each article, the analysis of the terms of reference of each strategy as part of the documentary research, the application forms covering 40 families benefited, and interviews based on comprehensive analysis of the speech. This study is divided into 02 articles, where the first is a discussion held on collective action and environmental sustainability, and the second is held a discussion about the sustainability of the initiatives underway to access water. The results of the discussion held on 02 articles that had their empirical built from the experience of the Commonwealth of Pendências dos Emídios revealed how far will the ability of the State to promote collective action and the limitations of the perception of sustainability that permeates these initiatives in the search for democratic access to water in semi-arid

Processos aleatórios não-markovianos: perfis de memória

One of the mechanisms responsible for the anomalous diffusion is the existence of long-range temporal correlations, for example, Fractional Brownian Motion and walk models according to Elephant memory and Alzheimer profiles, whereas in the latter two cases the walker can always "remember" of his first steps. The question to be elucidated, and the was the main motivation of our work, is if memory of the historic initial is condition for observation anomalous diffusion (in this case, superdiffusion). We give a conclusive answer, by studying a non-Markovian model in which the walkers memory of the past, at time t, is given by a Gaussian centered at time t=2 and standard deviation t which grows linearly as the walker ages. For large widths of we find that the model behaves similarly to the Elephant model; In the opposite limit (! 0), although the walker forget the early days, we observed similar results to the Alzheimer walk model, in particular the presence of amnestically induced persistence, characterized by certain log-periodic oscillations. We conclude that the memory of earlier times is not a necessary condition for the generating of superdiffusion nor the amnestically induced persistence and can appear even in profiles of memory that forgets the initial steps, like the Gausssian memory profile investigated here.