Contribuições para o processo de verificação de satisfatibilidade módulo teoria em Event-B

Event-B is a formal method for modeling and verification of discrete transition systems. Event-B development yields proof obligations that must be verified (i.e. proved valid) in order to keep the produced models consistent. Satisfiability Modulo Theory solvers are automated theorem provers used to verify the satisfiability of logic formulas considering a background theory (or combination of theories). SMT solvers not only handle large firstorder formulas, but can also generate models and proofs, as well as identify unsatisfiable subsets of hypotheses (unsat-cores). Tool support for Event-B is provided by the Rodin platform: an extensible Eclipse based IDE that combines modeling and proving features. A SMT plug-in for Rodin has been developed intending to integrate alternative, efficient verification techniques to the platform. We implemented a series of complements to the SMT solver plug-in for Rodin, namely improvements to the user interface for when proof obligations are reported as invalid by the plug-in. Additionally, we modified some of the plug-in features, such as support for proof generation and unsat-core extraction, to comply with the SMT-LIB standard for SMT solvers. We undertook tests using applicable proof obligations to demonstrate the new features. The contributions described can potentially affect productivity in a positive manner.

Características físico-químicas, sensoriais e perfil de ácidos graxos do leite de cabras saanen alimentadas com cactáceas

The objective of this research was to evaluate the influence of the supply of five types of native and exotic cacti Brazilian semiarid northeast on the sensory characteristics of milk of Saanen goats. Five multiparous goats were used with nine weeks of lactation, average live weight of 50 kg ± 4 kg., confined and distributed in a Latin square design 5 x 5 with five experimental diets and five periods. Each period lasted 17 days, with 10 days of adaptation to the diets of the animals and seven days for the data collection. The treatments were defined based on dry matter consisted of: 47.33 to 50.12% of a cactus (“Xiquexique”, “Mandacaru”, “Facheiro” or two species of forage cactus “Miúda” or “Orelha de Elefante Mexicana”) more 18.78 to 19.79% hay of plant “Sabiá” and 31.10 to 32.89% of concentrate. There was not effect of the experimental diets in the physical and chemical composition of milk for fat, total solids and salts, which showed mean values of 3.24%; 11.30% and 0.66%, respectively. However the protein, lactose, nonfat dry extract and freezing point were affected by diets. In the profile of fatty acids was higher concentration of fatty short and medium chain fatty acids, however, there were not changes between treatments, except for the butyric acid (C4:0), with mean values of 4.24% (“Orelha de Elefante Mexicana”) to 6.05% (“Facheiro”). The diets also did not provide sensory changes in milk for the parameters: odor, flavor, aftertaste and overall assessment. The use of the five cactus in the diet of dairy goats do not influence the sensory characteristics and lipid profile of milk. The physical and chemical composition of milk was showed within the minimum requirements of current legislation, except for nonfat dry extract and freezing point.

Implementação da infra-estrutura e protocolo de comunicação para tratamento e disponibilização de dados do projeto ePoste

The study consists in the structure elaboration and the ePoste project communicationprotocol, which is a system of monitoring by wireless communication with the aim tosensor and act with one or many public lighting points, and also the treatment of data todetect the activity in the sensors located on the posts. Previously the communication withsensors were made in locus and when data collect was necessary or the performance inthe devices, the operator had to move until the net place. Accordingly, the purpose has theconcern to increase the system dynamic, achieving the possible integrations with the systemsalready available to the lighting management. The same technology of communicationbetween the sensors are considerate, using the ZigBee protocol running on the meshnet, the communication with this net is made be internet through a gateway by GPRS,device with two basics functionalities, which bypass for data and the firmware update inthe sensor. This functionality test of data management is being tested; integrate way withlocal net of sensors and the internet data server operates. The protocol developed, besidesincorporating the ZigBee, that it is formation of framework in lower level, where definesbeginning, size and errors check, as well as the communication of sensor with the concentrator,which it is encapsulated in ZigBee; also the protocol of upper level, where thatit is the names, it was developed a platform of service to meet GET and POST requestsbeneath HTTP protocol, this service is implemented in the data server, which availablethe communication with the clients systems, in case, lighting management systems.

Spondias tuberosa Arr. (UMBU): estudo fitoquímico e avaliação do potencial anti-inflamatório

Spondias tuberosa Arruda (Anacardiaceae) is a fruitful tree popularly known as umbuzeiro, tapereba or umbu. It is a native and endemic species from Brazil, widespread in Brazilian Northeast. The species is important in folk medicine of the semi-arid Northeast, where it is mainly used to treat various inflammatory conditions, digestive problems as well as viral and bacterial infections. However, despite the common use in folk medicine, there are scarce pharmacological and phytochemicals studies that afford scientific evidence to its popular use. Therefore, this study aimed to characterize the chemical markers in S. tuberosa leaves extract, obtained by maceration ethanol:water (70:30, [v/v]), and evaluate its anti-inflammatory potential in vivo. The phytochemical profile in TLC analysis suggested the occurence of the flavonoids rutin and isoquercitrin. HPLC analysis enabled us to confirm the presence of flavonoids and also, were detected the phenolic acids, chlorogenic acid and caffeic acid. In addition was developed and validated a HPLC method to evaluate the content of the identified compounds in S. tuberosa leaves extract according to RDC 899/2003 of ANVISA and ICH Guidelines 2005. In order to evaluate the anti-inflammatory potential of S. tuberosa leaves extract, the peritonitis and paw edema models induced by carrageenan were used, administration i.p. in mice. The results highlighted the anti-inflammatory property in vivo at 125, 250 and 500 mg/kg since a decrease in leukocyte influx to the site of inflammation, diameter of the edema and the level of myeloperoxidase were observed when compared to the drug control dexamethasone (2 mg/kg, i.p. route). Taken together, the results pointed out S. tuberosa as a potential species for developing phytotherapic derivatives in according to its popular use. With regard to the characterization markers, chlorogenic acid, caffeic acid, rutin and isoquercitrin were identified and quantified in Spondias tuberosa leaves extract so they could be used in quality control analyses of the raw material and extracts of this species.

Lâminas de água salina e doses de adubação orgânica na produção de palma Miúda adensada no semiárido

Cactus pear is an important forage for livestock in semi-arid region of Brazil, due to its adaptation to climate conditions in this region, high productivity and nutritional value. The yield of this cactus has positively responded to techniques such as planting density, fertilization and cutting managements, however, in Rio Grande do Norte State, only certain areas have favorable climate conditions to the development of this crop. Drip irrigation, with a small amount of water, has proven to be an alternative to the viability of cactus pear cultivation in these areas. The research aimed to evaluate the effects of different levels of saline water and manure organic fertilization on the morphological characteristics and production of fresh and dry matter of the prickly-pear cactus cv. Miúda (Nopalea cochenillifera Salm Dick) in a dense planting system. The experiment was conducted at the Experimental Station of Terras Secas (EMPARN), Pedro Avelino, latitude 5°31'21" South and longitude 36°23'14" West. The soil was classified as Typical Cambisol Haplicum Carbonate and the water used in irrigation, C4S1T3 (5,25 dS.m-1), with planting spacing of 2.0 x 0.25 m (20,000 plants ha-1). A completely randomized design in a split plot was used, where water levels (0, 7.5, 15.0 and 30.0 mm month-1) with 10 days intervals, were the main plots and organic fertilization (0 , 25 and 50 Mg ha-1 yr-1) the subplots, with four replicates. The measured morphological characteristics were number of cladodes, height and volume of the plant; length, width, perimeter, thickness, area and cladodes area index, fresh and dry matter production, dry matter content, water use efficiency (WUE) and damage promoted by cochineal pest (Diaspis echinocacti) and soft rot (Erwinia carotovora). There was no influence (P>0.05) of organic fertilization on most variables, particularly in relation to the production of fresh and dry matter. The water levels had a significant influence (P<0.05) on most variables, promoting higher height and volume of the plants, larger and thicker cladodes, and increase on fresh and dry matter production (13.55 Mg DM ha-1 yr-1). The absence of irrigation caused a significant expansion in plant damage caused by the cochineal pest and when irrigated with different water levels there was an increase in damage and stand loss, caused by soft rot, been more intense at the higher water level.

Avaliação do desempenho da paligorsquita modificada e do carvão da pirólise do lodo de esgoto no processo de degradação fotocatalítica do fenol

The uncontrolled disposal of wastewaters containing phenolic compounds by the industry has caused irreversible damage to the environment. Because of this, it is now mandatory to develop new methods to treat these effluents before they are disposed of. One of the most promising and low cost approaches is the degradation of phenolic compounds via photocatalysis. This work, in particular, has as the main goal, the customization of a bench scale photoreactor and the preparation of catalysts via utilization of char originated from the fast pyrolysis of sewage sludge. The experiments were carried out at constant temperature (50°C) under oxygen (410, 515, 650 and 750 ml min-1). The reaction took place in the liquid phase (3.4 liters), where the catalyst concentration was 1g L-1 and the initial concentration of phenol was 500 mg L-1 and the reaction time was set to 3 hours. A 400 W lamp was adapted to the reactor. The flow of oxygen was optimized to 650 ml min-1. The pH of the liquid and the nature of the catalyst (acidified and calcined palygorskite, palygorskite impregnated with 3.8% Fe and the pyrolysis char) were investigated. The catalytic materials were characterized by XRD, XRF, and BET. In the process of photocatalytic degradation of phenol, the results showed that the pH has a significant influence on the phenol conversion, with best results for pH equal to 5.5. The phenol conversion ranged from 51.78% for the char sewage sludge to 58.02% (for palygorskite acidified calcined). Liquid samples analyzed by liquid chromatography and the following compounds were identified: hydroquinone, catechol and maleic acid. A mechanism of the reaction was proposed, whereas the phenol is transformed into the homogeneous phase and the others react on the catalyst surface. For the latter, the Langmuir-Hinshelwood model was applied, whose mass balances led to a system of differential equations and these were solved using numerical methods in order to get estimates for the kinetic and adsorption parameters. The model was adjusted satisfactorily to the experimental results. From the proposed mechanism and the operating conditions used in this study, the most favored step, regardless of the catalyst, was the acid group (originated from quinone compounds), being transformed into CO2 and water, whose rate constant k4 presented value of 0.578 mol L-1 min-1 for acidified calcined palygorskite, 0.472 mol L-1 min-1 for Fe2O3/palygorskite and 1.276 mol L-1 min-1 for the sludge to char, the latter being the best catalyst for mineralization of acid to CO2 and water. The quinones were adsorbed to the acidic sites of the calcined palygorskite and Fe2O3/palygorskite whose adsorption constants were similar (~ 4.45 L mol-1) and higher than that of the sewage sludge char (3.77 L mol-1).

Avaliação do desempenho da paligorsquita modificada e do carvão da pirólise do lodo de esgoto no processo de degradação fotocatalítica do fenol

The uncontrolled disposal of wastewaters containing phenolic compounds by the industry has caused irreversible damage to the environment. Because of this, it is now mandatory to develop new methods to treat these effluents before they are disposed of. One of the most promising and low cost approaches is the degradation of phenolic compounds via photocatalysis. This work, in particular, has as the main goal, the customization of a bench scale photoreactor and the preparation of catalysts via utilization of char originated from the fast pyrolysis of sewage sludge. The experiments were carried out at constant temperature (50°C) under oxygen (410, 515, 650 and 750 ml min-1). The reaction took place in the liquid phase (3.4 liters), where the catalyst concentration was 1g L-1 and the initial concentration of phenol was 500 mg L-1 and the reaction time was set to 3 hours. A 400 W lamp was adapted to the reactor. The flow of oxygen was optimized to 650 ml min-1. The pH of the liquid and the nature of the catalyst (acidified and calcined palygorskite, palygorskite impregnated with 3.8% Fe and the pyrolysis char) were investigated. The catalytic materials were characterized by XRD, XRF, and BET. In the process of photocatalytic degradation of phenol, the results showed that the pH has a significant influence on the phenol conversion, with best results for pH equal to 5.5. The phenol conversion ranged from 51.78% for the char sewage sludge to 58.02% (for palygorskite acidified calcined). Liquid samples analyzed by liquid chromatography and the following compounds were identified: hydroquinone, catechol and maleic acid. A mechanism of the reaction was proposed, whereas the phenol is transformed into the homogeneous phase and the others react on the catalyst surface. For the latter, the Langmuir-Hinshelwood model was applied, whose mass balances led to a system of differential equations and these were solved using numerical methods in order to get estimates for the kinetic and adsorption parameters. The model was adjusted satisfactorily to the experimental results. From the proposed mechanism and the operating conditions used in this study, the most favored step, regardless of the catalyst, was the acid group (originated from quinone compounds), being transformed into CO2 and water, whose rate constant k4 presented value of 0.578 mol L-1 min-1 for acidified calcined palygorskite, 0.472 mol L-1 min-1 for Fe2O3/palygorskite and 1.276 mol L-1 min-1 for the sludge to char, the latter being the best catalyst for mineralization of acid to CO2 and water. The quinones were adsorbed to the acidic sites of the calcined palygorskite and Fe2O3/palygorskite whose adsorption constants were similar (~ 4.45 L mol-1) and higher than that of the sewage sludge char (3.77 L mol-1).

Uma interface para o controle de robôs móveis por intermédio de gestos

The main objective of this work was to enable the recognition of human gestures through the development of a computer program. The program created captures the gestures executed by the user through a camera attached to the computer and sends it to the robot command referring to the gesture. They were interpreted in total ve gestures made by human hand. The software (developed in C ++) widely used the computer vision concepts and open source library OpenCV that directly impact the overall e ciency of the control of mobile robots. The computer vision concepts take into account the use of lters to smooth/blur the image noise reduction, color space to better suit the developer's desktop as well as useful information for manipulating digital images. The OpenCV library was essential in creating the project because it was possible to use various functions/procedures for complete control lters, image borders, image area, the geometric center of borders, exchange of color spaces, convex hull and convexity defect, plus all the necessary means for the characterization of imaged features. During the development of the software was the appearance of several problems, as false positives (noise), underperforming the insertion of various lters with sizes oversized masks, as well as problems arising from the choice of color space for processing human skin tones. However, after the development of seven versions of the control software, it was possible to minimize the occurrence of false positives due to a better use of lters combined with a well-dimensioned mask size (tested at run time) all associated with a programming logic that has been perfected over the construction of the seven versions. After all the development is managed software that met the established requirements. After the completion of the control software, it was observed that the overall e ectiveness of the various programs, highlighting in particular the V programs: 84.75 %, with VI: 93.00 % and VII with: 94.67 % showed that the nal program performed well in interpreting gestures, proving that it was possible the mobile robot control through human gestures without the need for external accessories to give it a better mobility and cost savings for maintain such a system. The great merit of the program was to assist capacity in demystifying the man set/machine therefore uses an easy and intuitive interface for control of mobile robots. Another important feature observed is that to control the mobile robot is not necessary to be close to the same, as to control the equipment is necessary to receive only the address that the Robotino passes to the program via network or Wi-Fi.

Sexualidade e saúde mental: construindo sentidos entre pessoas usuárias de um CAPS

When expressed by mental health services users, sexuality is typically denied by professionals, viewed as another symptom or as if these people are not capable of practicing it. Once Brazilian health professionals haven’t shown lots of investment in this theme, and few are the studies in this field, it is necessary the attention to be focused on researches involving this public. Therefore, the main goal of this study was understand the meanings of sexuality of the mental health services users, which were negotiated in sexuality workshops. The secondary goals were: a) understand the meanings of themes about sexuality brought by users through their experiences of everyday life; b) to evaluate the facilitating experience of the workshops on sexuality at CAPS. Thus, 10 workshops on sexuality were held, with an average of an hour and twenty minutes each, distributed from December 2014 and April 2015. There were 43 participants, 29 women and 14 men. The meetings had the following central themes: sexuality; sexuality and mental health; myths, beliefs and sexual taboos; gender identity; sexual orientation; sexual and reproductive rights; safe sex; and STD/AIDS. The data collection was through audio-recording of these meetings. Later, was made the transcript of the workshops, a careful reading of these transcripts and then its analysis. It was identified categories to analyze the interfaces that permeate the focus of the study. Initially, the categories relating to mental health and sexuality: meanings about sexuality; gender issues; gender and religion; sexual rights, STD/AIDS prevention and attention or denial of sexuality at CAPS. Later, those relating to the workshops facilitating process: challenges in facilitating the workshops; and the perception of the participants. A variety of meanings about sexuality could be noticed in the users’ statements, relating it more with affection and respect than with intercourse. The gender issues that emerged during the workshops were related to marital relationship, sexism, domestic violence, psychological violence and male and female roles in society. Moreover, were also revealed some situations that associated gender differences with religious issues, such as the submission of women and homosexuality. It was also noticed some experiences of the participants involving worrying situations of family violence, suicidal ideation and chemical castration, were often mismanaged or ignored by the service professionals. With regard to the facilitation of the workshops, it was possible to legitimize it as places where users were able to talk openly about the suggested themes and highlight its importance to the study site. Besides, it’s possible to list a few challenges of its facilitation in a mental health service, which was in general positively evaluated by the participants. Thus, the research highlights the need for sexuality theme discussion in mental health services, in order to understand, discuss and inform the users. Also, it’s important to problematize the stigma created in the theme relation with the users, the professionals and the society, working its specificities and avoiding a pathological bias.

Chemistry of eastern tropical Atlantic porewater

Distributions of pore water O2, NO-2, NO-3, NH+4, Si(OH)4, PO[3-]4, Mn[2+], F-, and T.A. were determined at 15 stations in the eastern equatorial Atlantic. While overall profile characteristics are consistent with previous models of organic matter diagenesis, profile shapes suggest that a deep reaction layer, rich in organic C, is also present at many sites. While it is unlikely that the oxidation of organic C in this layer has had a major effect on the ocean C cycle, pore water profile shapes are significantly altered. Despite exposure to seawater SO[2-]4 concentrations for > 1000 years, decomposition of the organic matter in the layer appears to be restricted to oxic and suboxic processes. These results suggest major differences in organic carbon decomposition and preservation under oxic/suboxic and anoxic conditions. Present-day benthic fluxes are largest adjacent to the eastern boundary coastal upwelling region and similar in magnitude to values reported for the eastern Pacific. Preliminary estimates suggest that the benthic respiration in the eastern 1/3 of the North Atlantic south of 20°N may alone account for >20% of the total deep North Atlantic respiration. Combining these results with estimates of organic C burial and deep water-column decomposition suggests that this region is a major location of organic C input into the deep sea.

The relationship between vegetation and modern pollen assemblages on Mount Paggeo (NE Greece)

In this study, we investigated the relationship between vegetation and modern-pollen rain along the elevational gradient of Mount Paggeo. We apply multivariate data analysis to assess the relationship between vegetation and modern-pollen rain and quantify the representativeness of forest zones. This study represents the first statistical analysis of pollen-vegetation relationship along an elevational gradient in Greece. Hence, this paper improves confidence in interpretation of palynological records from north-eastern Greece and may refine past climate reconstructions for a more accurate comparison of data and modelling. Numerical classification and ordination were performed on pollen data to assess differences among plant communities that beech (Fagus sylvatica) dominates or co-dominates. The results show a strong relationship between altitude, arboreal cover, human impact and variations in pollen and nonpollen palynomorph taxa percentages.

The European Union Foreign Policy in the Caucasus and Central Asia: The Limitations of the Opening towards the East

This article intends to study the evolution of the European Union foreign policy in the Southern Caucasus and Central Area throughout the Post-Cold War era. The aim is to analyze Brussels’ fundamental interests and limitations in the area, the strategies it has implemented in the last few years, and the extent to which the EU has been able to undermine the regional hegemons’ traditional supremacy. As will be highlighted, the Community’s chronic weaknesses, the local determination to preserve sovereignty and an increasing international geopolitical competition undermine any European aspiration to become a pre-eminent actor at the heart of the Eurasian continent in the near future.

Measuring children’s experience of their right to participate in school and community: a rights-based approach

This paper discusses the development of a children’s rights-based measure of participation and the findings from its use in a survey of 10 to 11 year old children (n= 3773). The measure, which was developed in collaboration with a group of children, had a high reliability (Cronbach’s alpha = .89). Findings suggest that children’s positive experience of their participation rights is higher in school than in community, and higher for girls compared to boys. It is argued that involving children in the ‘measurement’ of their own lives has the potential to generate more authentic data on children’s lived experiences.

Práticas de ensino da música de rabeca no Rio Grande do Norte

MARTINS, Emerson Carpegianne de Souza ; LIMA, Agostinho Jorge de. Práticas de ensino da música de rabeca no Rio Grande do Norte. In: ENCONTRO REGIONAL DA ABEM NORDESTE, 9. Natal, 2010.Anais... Natal: UFRN/ESCOLA DE MUSICA, 2010