Verificação formal automatizada para sistemas de raciocínio procedural (PRS) utilizando redes de petri coloridas (RPC)

Este trabalho apresenta uma técnica de verificação formal de Sistemas de Raciocínio Procedural, PRS (Procedural Reasoning System), uma linguagem de programação que utiliza a abordagem do raciocínio procedural. Esta técnica baseia-se na utilização de regras de conversão entre programas PRS e Redes de Petri Coloridas (RPC). Para isso, são apresentadas regras de conversão de um sub-conjunto bem expressivo da maioria da sintaxe utilizada na linguagem PRS para RPC. A fim de proceder fia verificação formal do programa PRS especificado, uma vez que se disponha da rede de Petri equivalente ao programa PRS, utilizamos o formalismo das RPCs (verificação das propriedades estruturais e comportamentais) para analisarmos formalmente o programa PRS equivalente. Utilizamos uma ferramenta computacional disponível para desenhar, simular e analisar as redes de Petri coloridas geradas. Uma vez que disponhamos das regras de conversão PRS-RPC, podemos ser levados a querer fazer esta conversão de maneira estritamente manual. No entanto, a probabilidade de introdução de erros na conversão é grande, fazendo com que o esforço necessário para garantirmos a corretude da conversão manual seja da mesma ordem de grandeza que a eliminação de eventuais erros diretamente no programa PRS original. Assim, a conversão automatizada é de suma importância para evitar que a conversão manual nos leve a erros indesejáveis, podendo invalidar todo o processo de conversão. A principal contribuição deste trabalho de pesquisa diz respeito ao desenvolvimento de uma técnica de verificação formal automatizada que consiste basicamente em duas etapas distintas, embora inter-relacionadas. A primeira fase diz respeito fias regras de conversão de PRS para RPC. A segunda fase é concernente ao desenvolvimento de um conversor para fazer a transformação de maneira automatizada dos programas PRS para as RPCs. A conversão automática é possível, porque todas as regras de conversão apresentadas seguem leis de formação genéricas, passíveis de serem incluídas em algoritmos

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

Preparation and characterization of new glassy system As2P2S8-Ga2S3

Glasses having the composition (100 - x)As2P2S8-xGa(2)S(3) with x ranging from 0 to 50% were investigated to determine the compositional effect on properties and local structure. The glass transition temperature (T-g) and the stability parameter against crystallization (T-x - T-g) increased with the addition of Ga2S3. The structure of these glasses was probed by Raman scattering, Fourier transform infrared (FT-IR) and P-31 nuclear magnetic resonance. on the basis of the observed vibrations and the strength of the P-31-P-31 homonuclear magnetic dipolar coupling, two scenarios can be proposed for the structural evolution induced by the addition of Ga2S3. For x <= 20% we may have the formation of GaS4E- groups (E = nonbonding electron), and for x >= 30% we have depolymerization of the As2P2S8 units and the formation of a network of GaPS4 units with each PS4/2 unit (Q(4)) species carrying a single positive formal charge.

Initial-condition problem for a chiral Gross-Neveu system

A time-dependent projection technique is used to treat the initial-value problem for self-interacting fermionic fields. On the basis of the general dynamics of the fields, we derive formal equations of kinetic-type for the set of one-body dynamical variables. A nonperturbative mean-field expansion can be written for these equations. We treat this expansion in lowest order, which corresponds to the Gaussian mean-field approximation, for a uniform system described by the chiral Gross-Neveu Hamiltonian. Standard stationary features of the model, such as dynamical mass generation due to chiral symmetry breaking and a phenomenon analogous to dimensional transmutation, are reobtained in this context. The mean-field time evolution of nonequilibrium initial states is discussed.

The Canadian retirement income system

Includes bibliography

O formal e o real na educação complementar de Araraquara/SP: o amargo da doce ilusão

Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq)

Do lar para o trabalho: um estudo sobre as representações sociais de mulheres que ficaram afastadas do mercado formal de trabalho por 10 anos

Pós-graduação em Serviço Social - FCHS

Avaliação comparativa entre a estimativa do impacto gerado por efluentes domésticos de assentamentos espontâneos e de ocupação formal na bacia do Tucunduba em Belém - Pará

A presente pesquisa apresenta avaliação comparativa do impacto ambiental gerado por contextos habitacionais diferentes dentro do mesmo espaço urbano, no caso o bairro do Guamá, município de Belém, o contexto formal corresponde à ocupação da Av. José Bonifácio e o contexto de produção informal corresponde à comunidade do Riacho Doce. Na referida avaliação foram levados em consideração para investigação os seguintes aspectos: Consumo per capita de água, consumo per capita de esgoto, universalidade e equidade do fornecimento dos serviços de saneamento (abastecimento de água e esgotamento sanitário), tarifação de abastecimento de água, qualidade e acessibilidade dos serviços, contexto habitacional, aspectos socioambientais, com objetivo de caracterizar a população residente nessas áreas e finalmente estimar a carga orgânica (Kg de DBO/dia) e a vazão (m3/d) de efluentes domésticos gerados de assentamentos espontâneos e em uma área urbana consolidada, com o intuito de identificar qual contexto habitacional apresenta maior potencial de impacto em termos de geração de vazão e carga orgânica sobre a bacia receptora de efluentes, neste caso a Bacia do Tucunduba. Apesar dos resultados serem valores relativamente próximos, na área de Assentamento Espontâneo, a vazão de esgotos estimada 44,38 m3/dia e Carga Orgânica de 13,31 Kg de DBO/dia, e na área de Ocupação Formal a vazão de esgotos estimada 43,06 m3/dia e Carga Orgânica de 12,91 Kg de DBO/dia, foi possível observar neste trabalho que existe diferenciação do impacto ambiental gerado pelas duas áreas na bacia receptora no Igarapé Tucunduba, sendo maior no Riacho Doce onde a população permanece em contato com os efluentes e sob maior vulnerabilidade sanitária, pois, os efluentes da José Bonifácio são encaminhados pela rede de drenagem e sua carga orgânica é diluída pela vazão de águas pluviais ao chegarem ao Igarapé (distanciando a contaminação de sua fonte) e os efluentes do Riacho Doce são lançados in natura diretamente sob as casas e no Igarapé.

Uma proposta linguística para o ensino da escrita formal para surdos brasileiros e portugueses

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

A Educação Não-Formal a partir dos relatórios da UNESCO

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

A geometria euclidiana na licenciatura em matemática do ponto de vista de professores formadores

Pós-graduação em Educação Matemática - IGCE

Husserl's two notions of completeness: husserl and hilbert on completeness and imaginary elements in mathematics

In this paper I discuss Husserl's solution of the problem of imaginary elements in mathematics as presented in the drafts for two lectures he gave in Göttingen in 1901 and other related texts of the same period, a problem that had occupied Husserl since the beginning of 1890, when he was planning a never published sequel to Philosophie der Arithmetik (1891). In order to solve the problem of imaginary entities Husserl introduced, independently of Hilbert, two notions of completeness (definiteness in Husserl's terminology) for a formal axiomatic system. I present and discuss these notions here, establishing also parallels between Husserl's and Hilbert's notions of completeness. © 2000 Kluwer Academic Publishers.

Quantification of Short and Medium Range Order in Mixed Network Former Glasses of the System GeO2-NaPO3: A Combined NMR and X-ray Photoelectron Spectroscopy Study

Glasses in the system xGeO(2)-(1-x)NaPO3 (0 <= x <= 0.50) were prepared by conventional melting quenching and characterized by thermal analysis, Raman spectroscopy, X-ray photoelectron spectroscopy (XPS), and P-31 nuclear magnetic resonance (MAS NMR) techniques. The deconvolution of the latter spectra was aided by homonuclear J-resolved and refocused INADEQUATE techniques. The combined analyses of P-31 MAS NMR and O-1s XPS lineshapes, taking charge and mass balance considerations into account, yield the detailed quantitative speciations of the phosphorus, germanium, and oxygen atoms and their respective connectivities. An internally consistent description is possible without invoking the formation of higher-coordinated germanium species in these glasses, in agreement with experimental evidence in the literature. The structure can be regarded, to a first approximation, as a network consisting of P-(2) and P-(3) tetrahedra linked via four-coordinate germanium. As implied by the appearance of P-(3) units, there is a moderate extent of network modifier sharing between phosphate and germanate network formers, as expressed by the formal melt reaction P-(2) + Ge-(4) -> P-(3) + Ge-(3). The equilibrium constant of this reaction is estimated as K = 0.52 +/- 0.11, indicating a preferential attraction of network modifier by the phosphorus component. These conclusions are qualitatively supported by Raman spectroscopy as well as P-31{Na-23} and P-31{Na-23} rotational echo double resonance (REDOR) NMR results. The combined interpretation of O-1s XPS and P-31 MAS NMR spectra shows further that there are clear deviations from a random connectivity scenario: heteroatomic P-O-Ge linkages are favored over homoatomic P-O-P and Ge-O-Ge linkages.

Essays on the Axiomatic Theory of Matching

This dissertation mimics the Turkish college admission procedure. It started with the purpose to reduce the inefficiencies in Turkish market. For this purpose, we propose a mechanism under a new market structure; as we prefer to call, semi-centralization. In chapter 1, we give a brief summary of Matching Theory. We present the first examples in Matching history with the most general papers and mechanisms. In chapter 2, we propose our mechanism. In real life application, that is in Turkish university placements, the mechanism reduces the inefficiencies of the current system. The success of the mechanism depends on the preference profile. It is easy to show that under complete information the mechanism implements the full set of stable matchings for a given profile. In chapter 3, we refine our basic mechanism. The modification on the mechanism has a crucial effect on the results. The new mechanism is, as we call, a middle mechanism. In one of the subdomain, this mechanism coincides with the original basic mechanism. But, in the other partition, it gives the same results with Gale and Shapley's algorithm. In chapter 4, we apply our basic mechanism to well known Roommate Problem. Since the roommate problem is in one-sided game patern, firstly we propose an auxiliary function to convert the game semi centralized two-sided game, because our basic mechanism is designed for this framework. We show that this process is succesful in finding a stable matching in the existence of stability. We also show that our mechanism easily and simply tells us if a profile lacks of stability by using purified orderings. Finally, we show a method to find all the stable matching in the existence of multi stability. The method is simply to run the mechanism for all of the top agents in the social preference.

Isolated Islands? Memory of the Holocaust in Formal and Non-Formal Education. The Case Study of Post-Communist Poland

Existing studies revealed several conflicts around the memory of the Holocaust in Poland: between understanding the need to teach about the Holocaust and indifference toward anti-Jewish graffiti; a conflict around the perception of Polish help to Jews; and the competing images of Polish and Jewish suffering during World War II. Those conflicts will be addressed in the paper as reflecting educational gaps in the Polish education system (lack of bad memory). This paper will look at the consciousness of young Poles, in terms of attitudes toward Jews, the Holocaust and memory of the Holocaust. The data presented are the preliminary results of the author’s longitudinal study „Attitudes of Young Poles toward the Jews and the Holocaust”. Quantitative and qualitative studies include field studies and participant observation of educational projects in Tykocin, Treblinka, Warsaw, Lublin, Bodzentyn and Kielce. The paper will present some components of the development of education about the Holocaust in Poland. There is a need to evaluate the attempt to bring back the memory of Jewish neighbours in some of the states of Central and Eastern Europe, a process with an ongoing effort to renovate monuments, destroyed cemeteries and synagogues. The number and scope of such initiatives in Poland indicate that civic institutions and individuals are intensifying their efforts to teach their fellow citizens about the Holocaust, however their impact should be assessed in detail.