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

GeOntoQuery - um mecanismo de busca em bancos de dados geográficos baseado em ontologias

Geographic Information System (GIS) are computational tools used to capture, store, consult, manipulate, analyze and print geo-referenced data. A GIS is a multi-disciplinary system that can be used by different communities of users, each one having their own interest and knowledge. This way, different knowledge views about the same reality need to be combined, in such way to attend each community. This work presents a mechanism that allows different community users access the same geographic database without knowing its particular internal structure. We use geographic ontologies to support a common and shared understanding of a specific domain: the coral reefs. Using these ontologies' descriptions that represent the knowledge of the different communities, mechanisms are created to handle with such different concepts. We use equivalent classes mapping, and a semantic layer that interacts with the ontologies and the geographic database, and that gives to the user the answers about his/her queries, independently of the used terms

Desenvolvimento de sistema magnético polimérico contendo antimicrobianos para tratamento de infecções por Helicobacter pylori

Helicobacter pylori is the main cause of gastritis, gastroduodenal ulcer disease and gastric cancer. The most recommended treatment for eradication of this bacteria often leads to side effects and patient poor compliance, which induce treatment failure. Magnetic drug targeting is a very efficient method that overcomes these drawbacks through association of the drug with a magnetic compound. Such approach may allow such systems to be placed slowed down to a specific target area by an external magnetic field. This work reports a study of the synthesis and characterization of polymeric magnetic particles loaded with the currently used antimicrobial agents for the treatment of Helicobacter pylori infections, aiming the production of magnetic drug delivery system by oral route. Optical microscopy, scanning electron microscopy, transmission electron microscopy, x-ray powder diffraction, nitrogen adsorption/desorption isotherms and vibrating sample magnetometry revealed that the magnetite particles, produced by the co-precipitation method, consisted of a large number of aggregated nanometer-size crystallites (about 6 nm), creating superparamagnetic micrometer with high magnetic susceptibility particles with an average diameter of 6.8 ± 0.2 μm. Also, the polymeric magnetic particles produced by spray drying had a core-shell structure based on magnetite microparticles, amoxicillin and clarithromycin and coated with Eudragit® S100. The system presented an average diameter of 14.2 ± 0.2 μm. The amount of magnetite present in the system may be tailored by suitably controlling the suspension used to feed the spray dryer. In the present work it was 2.9% (w/w). The magnetic system produced may prove to be very promising for eradication of Helicobacter pylori infections

Monitoramento ambiental da costa do Rio Grande do Norte com base em sensoriamento remoto e geodésia de precisão

This paper presents models of parameters of Sea Surface Layer (SSL), such as chlorophyll-a, sea surface temperature (SST), Primary Productivity (PP) and Total Suspended Matter (TSM) for the region adjacent to the continental shelf of Rio Grande do Norte (RN), Brazil. Concentrations of these parameters measured in situ were compared in time quasi-synchronous with images AQUA-MODIS between the years 2003 to 2011. Determination coefficients between samples in situ and bands reflectance sensor AQUA-MODIS were representative. From that, concentrations of SSL parameters were acquired for the continental shelf of the RN (eastern and northern) analyzing the geographic distribution of variation of these parameters between the years 2009-2012. Geographical and seasonal variations mainly influenced by global climate phenomena such as El Niño and La Niña, were found through the analysis of AQUA-MODIS images by Principal Components Analysis (PCA). Images show qualitatively the variance and availability of TSM in the regions, as well as their relationship with coastal erosion hotspots, monitored along the coast of the RN. In one of the areas identified as being of limited availability of TSM, we developed a methodology for assessment and evaluation of Digital Elevation Models (DEM) of beach surfaces (emerged and submerged sections) from the integration of topographic and bathymetric data measured in situ and accurately georeferenced compatible to studies of geomorphology and coastal dynamics of short duration. The methodology consisted of surveys with GNSS positioning operated in cinematic relative mode involved in topographic and bathymetric executed in relation to the stations of the geodetic network of the study area, which provided geodetic link to the Brazilian Geodetic System (GBS), univocal , fixed, and relatively stable over time. In this study Ponta Negra Beach, Natal / RN, was identified as a region with low variance and availability of MPS in the region off, as characterized by intense human occupation and intense coastal erosion in recent decades, which presents potential of the proposed methodology for accuracy and productivity, and the progress achieved in relation to the classical methods of surveying beach profiles

Poluentes atmosféricos: monóxido e dióxido de carbono no nordeste do Brasil

The interference of man in the middle atmosphere can be evidenced by the presence of carbon monoxide, gas associated with burning fossil fuels and carbon dioxide content, essential for respiration of plants and thermal balance of the Earth. In this thesis we initially evaluated the intensity of the spatial distribution of carbon monoxide in the Northeast of Brazil, and subsequently the behavior of temporal variations of the pollutants carbon monoxide and carbon dioxide in the atmospheric boundary layer Maxaranguape / RN. Research has shown that, driven by speculation and promoting the occupation of land for agriculture, cattle ranching and tourism in the Northeast of Brazil, the changes established by the man in the middle geomorphological affect the lower troposphere on a large scale, with a predominance of concentrations in central Pernambuco, Paraiba's south-central and central-west of Alagoas. However, the study of Maxaranguape / RN results showed little variation in carbon monoxide and carbon dioxide, with the speed of the wind persisting with values greater than 7.8 m / s, showing dispersion and diffusion of pollutants which resulted in faster renewal of local atmospheric air

Análise espectroscópica da estrela HD 150050: uma nova estrela gigante rica em lítio

Conselho Nacional de Desenvolvimento Científico e Tecnológico

Estudo do fluxo de neutrino solar com o código evolutivo de Toulouse - Geneva

The study of solar neutrinos is very important to a better comprehension of the set of nuclear reactions that occurs inside the Sun and in solar type stars. The ux of neutrinos provides a better comprehension of the stellar structure as a whole. In this dissertation we study the ux of neutrinos in a solar model, addressing the neutrino oscillation, analyzing with the intention of determining and verify the distribution from a statistical point of view, since this ux depends on the particles intrinsic velocity distributions in stellar plasma. The main tool for this analysis was the Toulouse-Geneva Stellar Evolution Code, or TGEC, which allow us to obtain the neutrino ux values per reaction and per layer inside the Sun, allowing us to compare the observational results for the neutrino ux detected on experiments based on Cl37 (Homestake), Ga71 (SAGE, Gallex/GNO) and water (SNO). Our results show the nal distribution for neutrino ux as a function of the depth using the coordinates of mass and radius. The dissertation also shows that the equations for this ux are present in TGEC.

Modelagem Matemática e Computacional de fenômenos eletrocinéticos em meios porosos carregados eletricamente

In this work we present a mathematical and computational modeling of electrokinetic phenomena in electrically charged porous medium. We consider the porous medium composed of three different scales (nanoscopic, microscopic and macroscopic). On the microscopic scale the domain is composed by a porous matrix and a solid phase. The pores are filled with an aqueous phase consisting of ionic solutes fully diluted, and the solid matrix consists of electrically charged particles. Initially we present the mathematical model that governs the electrical double layer in order to quantify the electric potential, electric charge density, ion adsorption and chemical adsorption in nanoscopic scale. Then, we derive the microscopic model, where the adsorption of ions due to the electric double layer and the reactions of protonation/ deprotanaç~ao and zeta potential obtained in modeling nanoscopic arise in microscopic scale through interface conditions in the problem of Stokes and Nerst-Planck equations respectively governing the movement of the aqueous solution and transport of ions. We developed the process of upscaling the problem nano/microscopic using the homogenization technique of periodic structures by deducing the macroscopic model with their respectives cell problems for effective parameters of the macroscopic equations. Considering a clayey porous medium consisting of kaolinite clay plates distributed parallel, we rewrite the macroscopic model in a one-dimensional version. Finally, using a sequential algorithm, we discretize the macroscopic model via the finite element method, along with the interactive method of Picard for the nonlinear terms. Numerical simulations on transient regime with variable pH in one-dimensional case are obtained, aiming computational modeling of the electroremediation process of clay soils contaminated

Monitoramento geoambiental do estuário do Rio Paraíba do Norte - PB por meio da cartografia temática digital e de produtos de sensoriamento remoto

The North Paraíba River Estuary, located in the eastern portion of the Paraíba State, Northeast Brazil, on coordinates 34º50 00 -34º57 30 S and 6º55 00 -7º7 30 W, constitutes a fluvio-marine plain formed by the North Paraíba River and its tributaries Sanhauá, Paroeira, Mandacaru, Tiriri, Tambiá, Ribeira and Guia. This estuary comprises an area of about 260 km2. Increasing human demands on the estuary area and inadequate environment managing have generated conflicts. The present work main purpose is to evaluate the geodynamic evolution of the North Paraíba River Estuary in the period from 1969 to 2001, using digital image processing techniques, thematic digital cartography and multitemporal data integration, combined to geological-geophysical field surveys. The SUDENE cartographic database, converted to digital format were, used to obtain occupation and topographic maps from 1969 and to generate a Digital Elevation Model (DEM). Digital Landsat 7 ETM+ and Spot HRVIR-PAN satellite images interpretation allowed the environmental characterization of the estuary. The most important digital processing results were achieved color composites RGB 5-4-3, 5-3-1, 5-2-NDWI and band ratio 7/4-5/3-4/2, 5/7-3/1-5/4). In addition the fusion image technique RGBI was used by the inclusion of the Spot HRVRI and Landsat 7 ETM+ panchromatic band on I layer with RGB triplets 5-4-3, 5-3-1 and 5/7-3/1-5/4. The DEM and digital images integration allowed the identification of seven geomorphological units: coastal tableland, flowing tray, tide plain, fluvial terrace, submerged dune, beach plain and beach). Both Side Scan Sonar and Echosound were used to analyse underwater surface and bedforms of the estuarine channel, sand predominance (fine to very fine) and 2D dune features 5 m wide and 0.5 m height. This investigation characterized the estuary as an environment dominated by regimen of average flow. The channel depth varies between 1 m and 11 m, being this last quota reached in the area of Porto de Cabedelo. The chanel estuary is relatively shallow, with erosion evidences mainly on its superior portion, attested by sand banks exposed during the low tide. Multitemporal digital maps from 1969 and 2001 integration were obtained through geoprocessing techniques, resulting the geodynamic evolution of the estuary based on landuse, DEM geomorphology and bathymetric maps

Estudo comparativo de abordagens de inversão do fator de qualidade Q

Seismic wave dispersion and attenuation studies have become an important tool for lithology and fluid discrimination in hydrocarbon reservoirs. The processes associated to attenuation are complex and are encapsulated in a single quantitative description called quality factor (Q). The present dissertation has the objective of comparing different approaches of Q determination and is divided in two parts. Firstly, we made performance and robustness tests of three different approaches for Q determination in the frequency domain. They are: peak shift, centroid shift and spectral ratio. All these tests were performed in a three-layered model. In the suite of tests performed here, we varied the thickness, Q and inclination of the layers for propagation pulses with central frequency of 30, 40 and 60 Hz. We found that the centroid shift method is produces robust results for the entire suíte of tests. Secondly, we inverted for Q values using the peak and centroid shift methods using an sequential grid search algorithm. In this case, centroid shift method also produced more robust results than the peak shift method, despite being of slower convergence

Caracterização sonográfica e sismoestratigráfica de alta resolução do estuário do Rio Potengi, Natal - RN

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