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.

Alquilação de tolueno com propeno, através de complexo ferro (II) ᵦ- diimina homogêneo e heterogeneizado em MCM-41, Al-MCM-41 e SBA-15

This work describes the synthesis and aplication of homogeneous and heterogenized iron catalysts in the alkylation reaction of toluene with propene, empolying experimental design. The homogenous complex was obtained trough the synthesis of the organic ligand folowed by the complexation of the iron(II) chloride. As to the heterogenized complexes, first were synthetized the inorganic supports (SBA-15, MCM-41 and Al-MCM-41). Then, it was synthetized the ligand again, that through funcionalization with chloropropyltrimethoxysilane (CPTMS), was anchored on the support previously calcinated. To these anchored ligands, was complexed the iron(II) chloride, previously solubilizated in tetrahydrofuran (THF). The organic ligand characterization was accomplished trough nuclear magnetic resonance (NMR) and Infrared spectroscopy (IV). The supports were characterized with x-ray diffraction (DRX), texture analysis with nitrogen adsorption/desorption (before and after the anchoring), termogravimetric analysis (TG) and infrared (IV). The metalic content was quantified trough the atomic absorption spectrophotometry (AAS). The complexes were tested in catalytic reactions emolying ethylaluminium sesquichloride (EASC) as co-catalyst in steel reactor, under mecanic stirring. The reaction conditions ranged from 4 to 36 ◦C, with many aluminum/iron ratios. The catalysts were actives in homogeneous and heterogenized ways. The homogenous catalytic complex showed a maximum turnover frequency (TOF) of 8.63 ×103 · h −1 , while, in some conditions, the anchored complexes showed better results, with TOF of until 8.08 ×103 · h −1 . Aditionally, it was possible to determine an equation, to the homogenous catalyst, that describes the product quantity in function of reacional temperature and aluminum/iron ratio.

Indicadores do nível relativo do mar e evolução costeira durante o holoceno tardio no litoral oeste do Ceará, NE do Brasil

In the coastal region of Ceará, between the municipalities of Acaraú and Itapipoca, thirteen sites were identified containing indicators of relative sea level, six of these being dated by optically stimulated luminescence (OSL) and radiocarbon. Ages obtained supports that were formed prograding beaches in the study area. In the eastern portion, beaches in coastal plain deposits occur while a system lagoon/barrier paleomangrove occurs in the western portion of the study area. In both cases the coastal deposits prograde from east to west. Higher sea levels were identified between the current: (a) 3.110-2.830 cal. yr. BP; (b) 1.830 yr. BP (OSL) - 1.490 cal. yr. BP; (c) between 1.240-1.060 cal. yr. BP; (d) 845-715 yr. BP (OSL). Since then the sea level suffered by lowering the current level. Variations in sea level are interpreted as responses to changes in the pattern of marine circulation and do not exclude possible tectonic disturbances in the basin of the continental margin. The indicators of relative sea level west coast of Ceará present differently from other curves constructed in the coastal northeast, suggesting that local factors mentioned above contributed to sea level fluctuations.

Avaliação da variação sedimentológica em uma área da plataforma continental sob a atuação da indústria petrolífera

Petroleum exploration activity occurs on the offshore Potiguar Basin, from very shallow (2-3 m) until about 50 m water depth, extending from Alto de Touros (RN) to Alto de Fortaleza (CE). Take in account the biological importance and the heterogeneity of sediments on this area, it is necessary the understanding of the sedimentological dynamics, and mainly the changes generated by petroleum exploration to prevent possible damages to environment. Despite the intense activity of oil exploration in this area, research projects like these are still rare. In view to minimize this gap, this study was developed to evaluate sedimentological, mineralogical and geochemical changes in the vicinity of a exploration well, here designated as well A, located on the Middle continental shelf, near the transition to Outer shelf. The well selected for this study was the first one drilled with Riserless Mud Recovery technology (RMR) in Brazil. The main difference from this to the conventional method is the possibility of drilling phase I of the well with return of drilling material to the rig tank, minimizing fluid and gravel discharging around the vicinity, during this phase. Monitoring consisted of three surveys, first of them done before start drilling, the second one done 19 days after the end of drilling and the third one done one year after then. Comparison of the studied variables (calcium carbonate and organic matter content, sediment size, mineralogy and geochemistry) was done with their average, median and coefficient of variation values to understand the changes after drilling activity. Because operating company technical reasons, the well location was changed after the first survey (C1), resulting in a shift of the sampled area on the two last surveys (C2 e C3). Nevertheless, the acquired data presented a good correlation, with no loss to the mean goal of the study. The sedimentological, mineralogical and geochemical analyzes were done at Federal University of Rio Grande do Norte (UFRN). The results indicated a predominantly sandy environment along the three surveys. It was noticed that the first survey (C1), presented different values for all the studied variables than to the second (C2) and third (C3) surveys, which had similar values. Siliciclastic sediments are prevalent at all surveys, and quartz is the main component (more than 80%). Heavy minerals (garnet, turmaline, zircon and lmenite), rock fragments and mud aggregates also was described. Bioclastic sediments are dominated by coralline algae (more than 45%) and mollusks (more than 30%), followed by benthic foraminifera, bryozoans and worm tubes. More rarely was observed ostracoda and spike of calcareous sponge. Because the low changes of the sediments at the studied area and by the using of RMR method in the drilling, it was possible to conclude that drilling activity did not promote significant alteration on the local sediment cover. Changes in the studied variables before and after drilling activity could be influenced by the changing in the sampling area after survey 1 (C1).

Uma linguagem de descrição arquitetural baseada em uma arquitetura de referência para sistemas ubíquos

A computação ubíqua é um paradigma no qual dispositivos com capacidade de processamento e comunicação são embutidos nos elementos comuns de nossas vidas (casas, carros, máquinas fotográficas, telefones, escolas, museus, etc), provendo serviços com um alto grau de mobilidade e transparência. O desenvolvimento de sistemas ubíquos é uma tarefa complexa, uma vez que envolve várias áreas da computação, como Engenharia de Software, Inteligência Artificial e Sistemas Distribuídos. Essa tarefa torna-se ainda mais complexa pela ausência de uma arquitetura de referência para guiar o desenvolvimento de tais sistemas. Arquiteturas de referência têm sido usadas para fornecer uma base comum e dar diretrizes para a construção de arquiteturas de softwares para diferentes classes de sistemas. Por outro lado, as linguagens de descrição arquitetural (ADLs) fornecem uma sintaxe para representação estrutural dos elementos arquiteturais, suas restrições e interações, permitindo-se expressar modelo arquitetural de sistemas. Atualmente não há, na literatura, ADLs baseadas em arquiteturas de referência para o domínio de computação ubíqua. De forma a permitir a modelagem arquitetural de aplicações ubíquas, esse trabalho tem como objetivo principal especificar UbiACME, uma linguagem de descrição arquitetural para aplicações ubíquas, bem como disponibilizar a ferramenta UbiACME Studio, que permitirá arquitetos de software realizar modelagens usando UbiACME. Para esse fim, inicialmente realizamos uma revisão sistemática, de forma a investigar na literatura relacionada com sistemas ubíquos, os elementos comuns a esses sistemas que devem ser considerados no projeto de UbiACME. Além disso, com base na revisão sistemática, definimos uma arquitetura de referência para sistemas ubíquos, RA-Ubi, que é a base para a definição dos elementos necessários para a modelagem arquitetural e, portanto, fornece subsídios para a definição dos elementos de UbiACME. Por fim, de forma a validar a linguagem e a ferramenta, apresentamos um experimento controlado onde arquitetos modelam uma aplicação ubíqua usando UbiACME Studio e comparam com a modelagem da mesma aplicação em SySML.

Algoritmo papílio como método de proteção de templates para aumentar a segurança em sistemas de identificação biométricos

There are authentication models which use passwords, keys, personal identifiers (cards, tags etc) to authenticate a particular user in the authentication/identification process. However, there are other systems that can use biometric data, such as signature, fingerprint, voice, etc., to authenticate an individual in a system. In another hand, the storage of biometric can bring some risks such as consistency and protection problems for these data. According to this problem, it is necessary to protect these biometric databases to ensure the integrity and reliability of the system. In this case, there are models for security/authentication biometric identification, for example, models and Fuzzy Vault and Fuzzy Commitment systems. Currently, these models are mostly used in the cases for protection of biometric data, but they have fragile elements in the protection process. Therefore, increasing the level of security of these methods through changes in the structure, or even by inserting new layers of protection is one of the goals of this thesis. In other words, this work proposes the simultaneous use of encryption (Encryption Algorithm Papilio) with protection models templates (Fuzzy Vault and Fuzzy Commitment) in identification systems based on biometric. The objective of this work is to improve two aspects in Biometric systems: safety and accuracy. Furthermore, it is necessary to maintain a reasonable level of efficiency of this data through the use of more elaborate classification structures, known as committees. Therefore, we intend to propose a model of a safer biometric identification systems for identification.

ArchWiSeN: uma estratégia baseada em modelos para desenvolvimento de aplicações para redes de sensores e atuadores sem fio

Wireless Sensor and Actuator Networks (WSAN) are a key component in Ubiquitous Computing Systems and have many applications in different knowledge domains. Programming for such networks is very hard and requires developers to know the available sensor platforms specificities, increasing the learning curve for developing WSAN applications. In this work, an MDA (Model-Driven Architecture) approach for WSAN applications development called ArchWiSeN is proposed. The goal of such approach is to facilitate the development task by providing: (i) A WSAN domain-specific language, (ii) a methodology for WSAN application development; and (iii) an MDA infrastructure composed of several software artifacts (PIM, PSMs and transformations). ArchWiSeN allows the direct contribution of domain experts in the WSAN application development without the need of specialized knowledge on WSAN platforms and, at the same time, allows network experts to manage the application requirements without the need for specific knowledge of the application domain. Furthermore, this approach also aims to enable developers to express and validate functional and non-functional requirements of the application, incorporate services offered by WSAN middleware platforms and promote reuse of the developed software artifacts. In this sense, this Thesis proposes an approach that includes all WSAN development stages for current and emerging scenarios through the proposed MDA infrastructure. An evaluation of the proposal was performed by: (i) a proof of concept encompassing three different scenarios performed with the usage of the MDA infrastructure to describe the WSAN development process using the application engineering process, (ii) a controlled experiment to assess the use of the proposed approach compared to traditional method of WSAN application development, (iii) the analysis of ArchWiSeN support of middleware services to ensure that WSAN applications using such services can achieve their requirements ; and (iv) systematic analysis of ArchWiSeN in terms of desired characteristics for MDA tool when compared with other existing MDA tools for WSAN.

Tecnologia eletroquímica como tratamento alternativo de efluentes derivados da indústria têxtil e petroquímica

In this work, the treatment of wastewater from the textile industry, containing dyes as Yellow Novacron (YN), Red Remazol BR (RRB) and Blue Novacron CD (NB), and also, the treatment of wastewater from petrochemical industry (produced water) were investigated by anodic oxidation (OA) with platinum anodes supported on titanium (Ti/Pt) and boron-doped diamond (DDB). Definitely, one of the main parameters of this kind of treatment is the type of electrocatalytic material used, since the mechanisms and products of some anodic reactions depend on it. The OA of synthetic effluents containing with RRB, NB and YN were investigated in order to find the best conditions for the removal of color and organic content of the dye. According to the experimental results, the process of OA is suitable for decolorization of wastewaters containing these textile dyes due to electrocatalytic properties of DDB and Pt anodes. Removal of the organic load was more efficient at DDB, in all cases; where the dyes were degraded to aliphatic carboxylic acids at the end of the electrolysis. Energy requirements for the removal of color during OA of solutions of RRB, NB and YN depends mainly on the operating conditions, for example, RRB passes of 3.30 kWh m-3 at 20 mA cm-2 for 4.28 kWh m-3 at 60 mA cm-2 (pH = 1); 15.23 kWh m-3 at 20 mA cm-2 to 24.75 kWh m-3 at 60 mA cm-2 (pH 4.5); 10.80 kWh m-3 at 20 mA cm-2 to 31.5 kWh m-3 at 60 mA cm-2 (pH = 8) (estimated data for volume of treated effluent). On the other hand, in the study of OA of produced water effluent generated by petrochemical industry, galvanostatic electrolysis using DDB led to the complete removal of COD (98%), due to large amounts of hydroxyl radicals and peroxodisulphates generated from the oxidation of water and sulfates in solution, respectively. Thus, the rate of COD removal increases with increasing applied current density (15-60 mAcm-2 ). Moreover, at Pt electrode, approximately 50% removal of the organic load was achieved by applying from 15 to 30 mAcm-2 while 80% of COD removal was achieved for 60 mAcm-2 . Thus, the results obtained in the application of this technology were satisfactory depending on the electrocatalytic materials and operating conditions used for removal of organic load (petrochemical and textile effluents) as well as for the removal of color (in the case of textile effluents). Therefore, the applicability of electrochemical treatment can be considered as a new alternative like pretreatment or treatment of effluents derived from textiles and petrochemical industries.

Síntese de carreadores de oxigênio à base de Ni e Co para estudo do processo de Chemical Looping usando CH4 como combustível

Increasing energy demand is being met largely by fossil fuel reserves, which emit CO2, SOx gases and various other pollutants. So does the search for fuels that emit fewer pollutants and have the same energy efficiency. In this context, hydrogen (H2) has been increasingly recognized as a potential carrier of energy for the near future. This is because the H2 can be obtained by different routes and has a wide application area , in addition to having clean burning, generating only H2O as a product of combustion , and higher energy density per unit mass . The Chemical Looping Reforming process (CLR) has been extensively investigated in recent years, it is possible to regenerate the catalyst by applying cycles of reduction and oxidation. This work has as main objective to develop catalysts based on nickel and cobalt to study the reactivity of reform with chemical recycling process. The catalysts were prepared by three different methods: combustion assisted by microwave, wet impregnation and co-precipitation. All catalysts synthesized have the same amount by weight of the active phases (60% w / w). The other 40 % m/m consists in La2O3 (8% w / w), Al2O3 (30% w / w) and MgO (2%). Oxygen carriers have been named as follows: N or C, nickel or cobalt, followed by the number 3 or 6, meaning 30 to 60% of active phase in the oxide form and C, CI or CP, which means self-combustion assisted by microwave, self-combustion assisted by microwave followed by wet impregnation and co-precipitation. The oxygen carriers were then characterized by the techniques of X-ray diffraction (XRD), surface area (BET), temperature programmed reduction (TPR) and scanning electron microscopy (SEM). The characterization results showed that the different synthesis methods have led to obtaining different morphologies and structures. Redox tests using CH4 as reducing agent and sintetic air as oxidant agent was done with N6C and C6C, N6CI and C6CI and N6CP and C6CP oxygen carriers. The tests revealed different behaviors, depending on active phase and on synthesis procedure. N6C oxygen carrier produced high levels of H2. The C6CI oxygen carrier produced CO2 and H2O without carbon deposits.

Caracterização morfológica-sedimentar do vale inciso Apodi-Mossoró e plataforma continental adjacente - Bacia Potiguar Offshore

Systems of incised valleys have been studied in different continental shelves, including the Brazilian continental margin. The interest to characterize this feature is given by the information that it can provide variations on sea level, as well as the ability to host economically significant quantities of hydrocarbons in reservoirs located in deposits filling of the incised valleys. This thesis has the overall objective to characterize the morphology and sedimentary cover of the incised valley Apodi-Mossoró, located in the Northern Continental shelf of Rio Grande do Norte state, adjacent to Areia Branca city. The methodology included the integration of satellite imagery, bathymetric data, sedimentological data, shallow seismic, and the identification of foraminifera. The results indicate that the ApodiMossró incised valley is currently formed by two channels, shallow channel and deep channel, which have distinct morphological and sedimentological characteristics. The deep channel has connection with one of the heads of the Apodi Canyon, located in the slope area. The acquisition, processing and interpretation of shallow seismic data allowed the recognition of the depositional surface, erosional surface, discordance, and sismofaceis. The erosional surface mapped from shallow seismic sections is possibly a indicative of an ancient surface of valley incision, where it would probably be associated with the limit Pleistocene/Holocene. Different sismofaceis were identified and reflect the rise in sea level with standards sometimes agradacional, sometimes progradational. The thickness of sediments on this surface was estimated at a maximum of 22m thick in the central portion of the incised valley. Statistically, there are differences between the adjacent continental shelf and channels, and between these channels, for the content of calcium carbonate, organic matter, sand and mud perceptual, except for the gravel grain size. The analysis of living and dead foraminifera showed the presence of fifty species distributed in regards to morphology, depth and type of sediment. Four type of seismic echocharacteres were identified and mapped, as well as their bedforms, indicating different sedimentary processes along the incised valley. The integration of results suggests an activation of the Apodi-Mossoró incised valley in the Late Pleistocene.

O paradoxo da superdifusão de uma caminhada aleatória com memória exponencial

The random walk models with temporal correlation (i.e. memory) are of interest in the study of anomalous diffusion phenomena. The random walk and its generalizations are of prominent place in the characterization of various physical, chemical and biological phenomena. The temporal correlation is an essential feature in anomalous diffusion models. These temporal long-range correlation models can be called non-Markovian models, otherwise, the short-range time correlation counterparts are Markovian ones. Within this context, we reviewed the existing models with temporal correlation, i.e. entire memory, the elephant walk model, or partial memory, alzheimer walk model and walk model with a gaussian memory with profile. It is noticed that these models shows superdiffusion with a Hurst exponent H > 1/2. We study in this work a superdiffusive random walk model with exponentially decaying memory. This seems to be a self-contradictory statement, since it is well known that random walks with exponentially decaying temporal correlations can be approximated arbitrarily well by Markov processes and that central limit theorems prohibit superdiffusion for Markovian walks with finite variance of step sizes. The solution to the apparent paradox is that the model is genuinely non-Markovian, due to a time-dependent decay constant associated with the exponential behavior. In the end, we discuss ideas for future investigations.

Influência da desordem estrutural nas propriedades magnéticas de filmes finos de Co2FeAl

Thin films of Co2FeAl (CFA) and trilayers with CFA/M/CFA, where M is Au or Ag, produced by magnetron sputtering onto glass and oriented (MgO (100)) substrates were investigated. The structural, magnetic static and magnetic dynamics properties were analyzed by distinct experimental techniques. Through X-ray diffraction was observed an A2 phase for the samples (completely disordered), where the atoms are randomly located in the lattice. The static magnetic behavior, in some samples, reveal a plateau behavior generated by a biphasic system. The magnetoimpedance measurements were performed by varying the angle between the external magnetic field and current with respect of anisotropy direction. For this reason, the MI results show a asymmetric magnetoimpedance (AMI) behavior. For the single and trilayers samples with 500 nm-thick, the AMI effect is more evident in comparison with samples with 1000 nm-thick. Therefore, in this work was stablished a route to produce Heusler alloy samples with A2 phase in thin film geometry onto amorphous and oriented substrates, and due to structural disorder was possible to study the hysteretic and MI asymmetric effects.

Desenvolvimento de aplicações móveis baseadas em sistemas de informações web existentes

Considerando a era da computação móvel percebe-se que os sistemas de informaçãoestão passando por um processo de metamorfose para possibilitar que seus usuários utilizemnovas formas de acessos às informações a partir de dispositivos móveis. Isso se deveprincipalmente ao aumento da popularidade de dispositivos como smartphones e tablets.Impulsionado por esse novo cenário de computação, que está mudando velhos hábitos ecriando novas maneiras da sociedade acessar informações que até então só eram acessíveisatravés de computadores tradicionais, crescem as demandas por aplicações móveis corporativas.Esse aumento é ocasionado pela necessidade das empresas garantirem aos seusclientes novas formas de interações com seus serviços. Dessa forma, esse trabalho tem oobjetivo de apresentar um estudo referente ao desenvolvimento de aplicações móveis eum processo denominado Metamorphosis, que provê um conjunto de atividades organizadasem três fases: requisitos, projeto e implantação, para auxiliar no desenvolvimentode aplicações móveis corporativas baseadas em sistemas de informações web existentes.

Utilizando comitês de classificadores para predição de rendimento escolar

Educational Data Mining is an application domain in artificial intelligence area that has been extensively explored nowadays. Technological advances and in particular, the increasing use of virtual learning environments have allowed the generation of considerable amounts of data to be investigated. Among the activities to be treated in this context exists the prediction of school performance of the students, which can be accomplished through the use of machine learning techniques. Such techniques may be used for student’s classification in predefined labels. One of the strategies to apply these techniques consists in their combination to design multi-classifier systems, which efficiency can be proven by results achieved in other studies conducted in several areas, such as medicine, commerce and biometrics. The data used in the experiments were obtained from the interactions between students in one of the most used virtual learning environments called Moodle. In this context, this paper presents the results of several experiments that include the use of specific multi-classifier systems systems, called ensembles, aiming to reach better results in school performance prediction that is, searching for highest accuracy percentage in the student’s classification. Therefore, this paper presents a significant exploration of educational data and it shows analyzes of relevant results about these experiments.

Mapeamento da isoterma de Curie na Bacia do Parnaíba estimada através da profundidade da base das fontes magnéticas

Located on the western edge of the Brazilian northeast, the Parnaíba Basin is an intra cratonic basin with oil production. This study aims at understanding its genesis and evolution, using aeromagnetic and gravity data. We used the spectral analysis of aeromagnetic data to map the depth to the bottom of the magnetic sources in order to assimilate this depth with the depth of the Curie isotherm, and infer the geothermal gradient. Using the spectral analysis technique, we succeeded in mapping the surface of the depth to the bottom of magnetic sources (SBFM), which marks the depth that occur magnetization. In the Parnaíba Basin the SBFM presented depths around -20,5 and -28,5 , which was consistent with an inversion of the same dataset using the technique of Magnetization Vector Inversion (MVI). Furthermore, SBFM topography correlates well with Moho depth, which was estimated from satellite gravimetric data from the GOCE mission (Gravity Field and Steady-State Ocean Circulation Explorer). Assuming that SBFM coincides with the Curie isotherm of magnetite (ICM), defined as the surface at which magnetite ( ) looses its ferromagnetic properties, it was possible to estimate the geothermal gradient. The geothermal gradient in the basin showed values between 19.2 and 26.5 , allowing to estimate the heat flow for the Parnaíba basin after assuming a conductivity of 2.69 . The resulting heat flow values ranged between 51.6 and 71.3 , which is consistent with values found in other works throughout the South American continent. Lithospheric thickness using an empirical relationship, finding values between -65.8 and -89.2 . We propose that thermal structure of Parnaíba basin is influenced by a deep thermal anomaly. This anomaly has heated the lithosphere beneath the basin and has resulted in relatively thin values for the lithospheric thickness and relatively high surface heat flow values. The origin of the anomaly is not clear, but the correlation between Curie depth and Moho topography, suggests that tectonic extension processes could have played a role.