Síntese e caracterização da ferrita de MnZn obtida pelo método dos citratos precursores

It was synthesized MnZn ferrite with general formulae Mn1-xZnxFe2O4 (mol%), 0,3 ≤ x ≤ 0,7 by using the citrate precursor method. The precursors decomposition was studied by thermogravimetric analysis (TGA), differential thermogravimetric analysis (DTG), differential thermal analysis (DTA) and Fourier transform infrared (FTIR) of powder calcined at 350ºC/3,5h. X-ray diffraction pattern (XRD) of samples was done from 350 to 1200ºC/2h using various atmospheres. The power calcined at 350ºC/3,5h formed spinel phase. It is necessary atmosphere control to avoid secondary phase such as hematite. From 900 to 1200ºC was obtained 90,66 and 100% of MnZn spinel ferrite phase, respectively. Analysis by dispersive energy scanning (EDS) at 350ºC shows high Mn and Zn dispersion, indicating that the diffusion process was homogeneous. Semi-quantitative analysis by EDS verified that despite the atmosphere control during calcinations at high temperatures (< 800ºC) occurred ZnO evaporation causing stoichiometric deviation. Vibrating sample magnetometer (VSM) measures show soft ferrite material characteristics with Hc from 6,5 x 10-3 to 11,1 x 10-2 T. Saturation magnetization (Ms) and initial permeability (µi) of MnZn spinel phase obtained, respectively, from 14,3 to 83,8 Am2/kg and 14,1 to 62,7 (Am2/kg)T

Aplicabilidade da voltametria de pulso diferencial na quantificação de ácido fólico e ácido oxálico: um método comparativo

The development of more selective and sensitive analytical methods is of great importance in different areas of knowledge, covering, for example, food, biotechnological, environmental and pharmaceutical sectors. The study aimed to employ the technique electroanalytical differential pulse voltammetry (DPV) as an innovative and promising alternative for identification and quantification of organic compounds. The organic compounds were investigated in this study oxalic acid (OA) and folic acid (FA). The electrochemical oxidation of oxalic acid has been extensively studied as a model reaction in the boundary between the organic and inorganic electrochemistry. Since the AF, an essential vitamin for cell multiplication in all tissues, which is essential for DNA synthesis. The AF has been investigated using analytical techniques, liquid chromatography and molecular absorption spectrophotometry. The results obtained during the experimental procedure indicated that the process of electrochemical oxidation of oxalic acid is strongly dependent on the nature of the anode material and the oxidation mechanism, which affects their detection. Efficient removal was observed in Ti/PbO2 anodes, graphite, BDD and Pt 90, 85, 80 and 78% respectively. It was also shown that the DPV employing glassy carbon electrode offers a fast, simple, reliable and economical way to determine the AO during the process of electrochemical oxidation. Furthermore, electroanalytical methods are more expensive than commonly used chromatographic analysis and other instrumental methods involving toxic reagents and higher cost. Compared with the classical method of titration and DPV could be a good fit, confidence intervals and detection limits confirming the applicability of electroanalytical technique for monitoring the degradation of oxalic acid. For the study of AF was investigated the electrocatalytic activity of the carbon paste electrode for identification and quantification in pharmaceutical formulations by applying the DPV. The results obtained during the experimental procedure showed an irreversible oxidation peak at 9.1 V characteristic of FA. The carbon paste sensor showed low detection limit of 5.683×10−8 mol L-1 reducing matrix effects. The spectrophotometric analysis showed lower concentrations of HF compared with those obtained by HPLC and DPV. The levels of AF were obtained according to the methodology proposed by the Brazilian Pharmacopoeia. The electroanalytical method (DPV) proposed is cheaper than GC analysis commonly used by the pharmaceutical industry. The results demonstrated the potential of these electroanalytical techniques for future applications in environmental, chemical and biological sensors

Passividade na interface prótese/pilar intermediário de infraestrutura implantossuportadas confeccionadas pela tecnologia CAD/CAM e método convencional

The objective of this research was to evaluate the passivity and strain induced in infrastructures screwed on abutments, made by CAD/CAM technology, and to compare these samples with parts manufactured by conventional casting. Using CAD/CAM technology, 4 samples were made from zirconia (Zircad) and 4 samples were manufactured from cobaltchrome (CoCrcad). The control groups were 4 specimens of cobalt-chrome, made by onepiece casting (CoCrci), for a total of 12 infrastructures. To evaluate the passivity, the infraestructures were installed on the abutments. One end was tightened and the vertical gap between the infrastructure and the prosthetic abutment was measured with scanning electron microscopy (250×). The mean strain in these infrastructures was analyzed via the photoelasticity test. A significant difference (p = 0.000) in passivity was observed between the control (CoCrci) and sample groups (CoCrcad and CoCrci). CoCrcad exhibited the best value of passivity (48.76 ± 13.45 μm) and CoCrci the worst (187.55 ± 103.63 μm), Zircad presented an intermediate value (103.81 ± 43.15 μm). When compared to the other groups, CoCrci showed the highest mean strain around the implants (17.19 ± 7.22 kPa). It was concluded that the zirconia infrastructure made by CAD / CAM showed a higher vertical marginal misfit than those made in cobalt-chromium alloy with the same methodology, however, the tension generated in the implants was similar. The CAD/CAM technology is more accurate for passivity and mean strain of infrastructure screwed on abutments than conventional manufacturing techniques

BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B

Java Card technology allows the development and execution of small applications embedded in smart cards. A Java Card application is composed of an external card client and of an application in the card that implements the services available to the client by means of an Application Programming Interface (API). Usually, these applications manipulate and store important information, such as cash and confidential data of their owners. Thus, it is necessary to adopt rigor on developing a smart card application to improve its quality and trustworthiness. The use of formal methods on the development of these applications is a way to reach these quality requirements. The B method is one of the many formal methods for system specification. The development in B starts with the functional specification of the system, continues with the application of some optional refinements to the specification and, from the last level of refinement, it is possible to generate code for some programming language. The B formalism has a good tool support and its application to Java Card is adequate since the specification and development of APIs is one of the major applications of B. The BSmart method proposed here aims to promote the rigorous development of Java Card applications up to the generation of its code, based on the refinement of its formal specification described in the B notation. This development is supported by the BSmart tool, that is composed of some programs that automate each stage of the method; and by a library of B modules and Java Card classes that model primitive types, essential Java Card API classes and reusable data structures

Prova automática de satisfatibilidade módulo teoria aplicada ao método B

Este trabalho apresenta uma extensão do provador haRVey destinada à verificação de obrigações de prova originadas de acordo com o método B. O método B de desenvolvimento de software abrange as fases de especificação, projeto e implementação do ciclo de vida do software. No contexto da verificação, destacam-se as ferramentas de prova Prioni, Z/EVES e Atelier-B/Click n Prove. Elas descrevem formalismos com suporte à checagem satisfatibilidade de fórmulas da teoria axiomática dos conjuntos, ou seja, podem ser aplicadas ao método B. A checagem de SMT consiste na checagem de satisfatibilidade de fórmulas da lógica de primeira-ordem livre de quantificadores dada uma teoria decidível. A abordagem de checagem de SMT implementada pelo provador automático de teoremas haRVey é apresentada, adotando-se a teoria dos vetores que não permite expressar todas as construções necessárias às especificações baseadas em conjuntos. Assim, para estender a checagem de SMT para teorias dos conjuntos destacam-se as teorias dos conjuntos de Zermelo-Frankel (ZFC) e de von Neumann-Bernays-Gödel (NBG). Tendo em vista que a abordagem de checagem de SMT implementada no haRVey requer uma teoria finita e pode ser estendida para as teorias nãodecidíveis, a teoria NBG apresenta-se como uma opção adequada para a expansão da capacidade dedutiva do haRVey à teoria dos conjuntos. Assim, através do mapeamento dos operadores de conjunto fornecidos pela linguagem B a classes da teoria NBG, obtem-se uma abordagem alternativa para a checagem de SMT aplicada ao método B

Especificação do micronúcleo FreeRTOS utilizando o método B

This paper presents a contribution to the international Verified Software Repository effort through the formal specification of the microkernel FreeRTOS real-time system. Such specification was made in abstract level making use of the B method . For thus, properties of the microkernel were chosen and selected as specification requisites, which was constructed centered at the functionalities responsible for the utilization of these properties. This properties weres setting as specification requirements. The specification was constructed modeling the function of microkernel that implement this properties. This work intended to encourage the formal verification of FreeRTOS and also contribute to the formal creation of a microkernel real-time systems, based in FreeRTOS. Furthermore, this model brings a formal documentation point view of the microkernel, demonstrating features and how this internal states is changing. Finally, this work could be an example of specification of the actual system by the B method.

KitSmart: Uma biblioteca de componentes para o desenvolvimento rigoroso de aplicações Java Card com o método B

The development of smart card applications requires a high level of reliability. Formal methods provide means for this reliability to be achieved. The BSmart method and tool contribute to the development of smart card applications with the support of the B method, generating Java Card code from B specifications. For the development with BSmart to be effectively rigorous without overloading the user it is important to have a library of reusable components built in B. The goal of KitSmart is to provide this support. A first research about the composition of this library was a graduation work from Universidade Federal do Rio Grande do Norte, made by Thiago Dutra in 2006. This first version of the kit resulted in a specification of Java Card primitive types byte, short and boolean in B and the creation of reusable components for application development. This work provides an improvement of KitSmart with the addition of API Java Card specification made in B and a guide for the creation of new components. The API Java Card in B, besides being available to be used for development of applications, is also useful as a documentation of each API class. The reusable components correspond to modules to manipulate specific structures, such as date and time. These structures are not available for B or Java Card. These components for Java Card are generated from specifications formally verified in B. The guide contains quick reference on how to specify some structures and how some situations were adapted from object-orientation to the B Method. This work was evaluated through a case study made through the BSmart tool, that makes use of the KitSmart library. In this case study, it is possible to see the contribution of the components in a B specification. This kit should be useful for B method users and Java Card application developers

Um método para desenvolvimento de abordagens generativas com composição de linguagens específicas de domínio

The software systems development with domain-specific languages has become increasingly common. Domain-specific languages (DSLs) provide increased of the domain expressiveness, raising the abstraction level by facilitating the generation of models or low-level source code, thus increasing the productivity of systems development. Consequently, methods for the development of software product lines and software system families have also proposed the adoption of domain-specific languages. Recent studies have investigated the limitations of feature model expressiveness and proposing the use of DSLs as a complement or substitute for feature model. However, in complex projects, a single DSL is often insufficient to represent the different views and perspectives of development, being necessary to work with multiple DSLs. In order to address new challenges in this context, such as the management of consistency between DSLs, and the need to methods and tools that support the development with multiple DSLs, over the past years, several approaches have been proposed for the development of generative approaches. However, none of them considers matters relating to the composition of DSLs. Thus, with the aim to address this problem, the main objectives of this dissertation are: (i) to investigate the adoption of the integrated use of feature models and DSLs during the domain and application engineering of the development of generative approaches; (ii) to propose a method for the development of generative approaches with composition DSLs; and (iii) to investigate and evaluate the usage of modern technology based on models driven engineering to implement strategies of integration between feature models and composition of DSLs

Um método semi-automatizado para elicitação de requisitos de acessibilidade Web

In the context of Software Engineering, web accessibility is gaining more room, establishing itself as an important quality attribute. This fact is due to initiatives of institutions such as the W3C (World Wide Web Consortium) and the introduction of norms and laws such as Section 508 that underlie the importance of developing accessible Web sites and applications. Despite these improvements, the lack of web accessibility is still a persistent problem, and could be related to the moment or phase in which this requirement is solved within the development process. From the moment when Web accessibility is generally regarded as a programming problem or treated when the application is already developed entirely. Thus, consider accessibility already during activities of analysis and requirements specification shows itself a strategy to facilitate project progress, avoiding rework in advanced phases of software development because of possible errors, or omissions in the elicitation. The objective of this research is to develop a method and a tool to support requirements elicitation of web accessibility. The strategy for the requirements elicitation of this method is grounded by the Goal-Oriented approach NFR Framework and the use of catalogs NFRs, created based on the guidelines contained in WCAG 2.0 (Web Content Accessibility Guideline) proposed by W3C

Método e sociologia em Weber: alguns conceitos fundamentais

Os parâmetros de análise social fornecidos pelos fundamentos da obra weberiana apontam algumas determinações necessárias à análise de fenômenos sociais. Defendendo uma sociologia capaz de compreender os sentidos e conexões presentes nas ações sociais, Weber propõe uma concepção específica de método e de objeto na sociologia, que se assenta na explicação de ações sociais individuais, sob condições determinadas, e busca, ao mesmo tempo, explicitar as significações das instituições sociais, nas quais os indivíduos agem, como resultantes também da ação humana. A partir de tais idéias, o breve ensaio ora apresentado, propõe-se a debater alguns elementos trabalhados nos conceitos weberianos de método e sociologia

Síntese e caracterização de pós Ba(x)Sr(1-x)Co0,8Fe0,2O3- através do método de coprecipitação via oxalato

Ceramic powders based on oxides of perovskite-type structure is of fundamental interest nowadays, since they have important ionic-electronic conductivity in the use of materials with technological applications such as gas sensors, oxygen permeation membranes, catalysts and electrolytes for solid oxide fuel cells (SOFC). The main objective of the project is to develop nanostructured ceramic compounds quaternary-based oxide Barium (Br), Strontium (Sr), Cobalt (Co) and Iron (Fe). In this project were synthesized compounds BaxSr(1-x)Co0, 8Fe0,2O3- (x = 0.2, 0.5 and 0.8) through the oxalate co-precipitation method. The synthesized powders were characterized by thermogravimetric analysis and differential thermal analysis (TGADTA), X-ray diffraction (XRD) with the Rietveld refinement using the software MAUD and scanning electron microscopy (SEM). The results showed that the synthesis technique used was suitable for production of nanostructured ceramic solid solutions. The powders obtained had a crystalline phase with perovskite-type structure. The TGA-DTA results showed that the homogeneous phase of interest was obtained temperature above 1034°C. It was also observed that the heating rate of the calcination process did not affect the elimination of impurities present in the ceramic powder. The variation in the addition of barium dopant promoted changes in the average crystallite size in the nanometer range, the composition being BSCF(5582) obtained the lowest value (179.0nm). The results obtained by oxalate co-precipitation method were compared with those synthesis methods in solid state and EDTA-citrate method

Método de Projeções Ortogonais

The problem treated in this dissertation is to establish boundedness for the iterates of an iterative algorithm in 2, under some technical conditions. However, this paper uses non-trivial intuitive arguments and its proofs lack suficient rigor. In this dissertation we discuss and strengthen the results of this paper, in order to complete and simplify its proofs

Aplicação do método B ao projeto formal de software embarcado

This work shows a project method proposed to design and build software components from the software functional m del up to assembly code level in a rigorous fashion. This method is based on the B method, which was developed with support and interest of British Petroleum (BP). One goal of this methodology is to contribute to solve an important problem, known as The Verifying Compiler. Besides, this work describes a formal model of Z80 microcontroller and a real system of petroleum area. To achieve this goal, the formal model of Z80 was developed and documented, as it is one key component for the verification upto the assembly level. In order to improve the mentioned methodology, it was applied on a petroleum production test system, which is presented in this work. Part of this technique is performed manually. However, almost of these activities can be automated by a specific compiler. To build such compiler, the formal modelling of microcontroller and modelling of production test system should provide relevant knowledge and experiences to the design of a new compiler. In ummary, this work should improve the viability of one of the most stringent criteria for formal verification: speeding up the verification process, reducing design time and increasing the quality and reliability of the product of the final software. All these qualities are very important for systems that involve serious risks or in need of a high confidence, which is very common in the petroleum industry