TELES, Liana Mara Rocha. Construção e validação de tecnologia educativa para acompanhantes durante o trabalho de parto e parto. 2011. 111 f. Dissertação (Mestrado em Enfermagem) - Universidade Federal do Ceará. Faculdade de Farmácia, Odontologia e Enfermagem, Fortaleza, 2011. / Submitted by denise santos (denise.santos@ufc.br) on 2013-12-19T13:49:25Z No. of bitstreams: 1 2011_dis_lmrteles.pdf: 1491445 bytes, checksum: bd66f1afaf6f4efb105c903246dd60de (MD5) / Approved for entry into archive by denise santos(denise.santos@ufc.br) on 2013-12-19T13:50:35Z (GMT) No. of bitstreams: 1 2011_dis_lmrteles.pdf: 1491445 bytes, checksum: bd66f1afaf6f4efb105c903246dd60de (MD5) / Made available in DSpace on 2013-12-19T13:50:35Z (GMT). No. of bitstreams: 1 2011_dis_lmrteles.pdf: 1491445 bytes, checksum: bd66f1afaf6f4efb105c903246dd60de (MD5) Previous issue date: 2011 / The present study aimed to build and validate a nursing educative technology (manual) directed for companions during labor and delivery. Methodological research developed in eleven stages. Begin, the five first regarding the construction of the manual, the following five referring to the validation process and, the last one, referring to the availability of the manual. The first stage corresponded to the content survey. In the second stage, there was a selection and written report of the raised content, in accordance with the demands of the companions. In the third stage, it was initiated textual elaboration. In the fourth stage, there was a raise of models, election and creation of 38 illustrations. The fifth stage corresponded to the layout of the manual, which was carried through according with the recommendations of the NBR6029 and developed through the program CorelDraw 15.0. After the five stages of construction of the educative manual, it was initiated the process of validation of the produced technology. In the sixth stage, nine specialists of the interest area were invited criteria in accordance with preset criteria (women’s health; obstetrics; technology in health; e instrument validation), which evaluated aims, structure and presentation, and relevance of the manual. A certain item was considered validated when it obtained a “Completely Adquetae” classification from at least half plus one of the number of specialists and Content Validity Index (CVI) higher or equal to 0,78. Some items were evaluated as satisfactory and others still need to suffer changes. As for the manual’s aim, specialists considered validated all questioned items, with an CVI between 0,88 and 1,0. As for structure and presentation of the manual, three items needed to adjust to the specialists suggestions: clarity and objectiveness of the messages; logic sequence of the content and match between writing and level of understanding of the target group. The CVI of the items that belong to this topic varied from 0,66 to 1,0. All items regarding the relevance of the manual were considered validated, with a CVI between 0,88 and 1,0. The global CVI of the educative manual was 0,94.. In the seventh stage, the educative manual was applied with eleven representatives of the target group obtained a level of conformity higher than 75% for the items evaluated such as organization, style of the writing, appearance and motivation of the manual. In the eighth stage, the alterations suggested from the specialists and representatives of the target group were accomplished: reformulating phrases, substitution of words or expressions; inclusion, substitution or relocation of information and illustration. The ninth stage corresponded to the review of the Portuguese by a specialized professional. In the tenth stage, the Flesch’s Index of Legibility was verified (FIL). The topics of the manual obtained a FIL between 50 and 94, which corresponds to an “Easy” or “Very Easy” reading, sufficient to a public with up to nine years of study. The last stage corresponded to printing of the manual. Finally, the educative manual validated by specialists and representatives of the target group is considered, regarding its appearance and content. Thus, further studies are necessary for the evaluation of the impact of this educative technology on the companion’s attitude in the labor room. / O presente estudo teve como objetivo construir e validar uma tecnologia educativa de enfermagem (manual) direcionada para acompanhantes durante o trabalho de parto e parto. Pesquisa metodológica desenvolvida em onze etapas, sendo as cinco primeiras correspondentes à construção do manual, as cinco seguintes referentes ao processo de validação e, a última, referente à disponibilização do manual. A primeira etapa correspondeu ao levantamento de conteúdo. Na segunda etapa, houve a seleção e fichamento do conteúdo levantado, de acordo com as demandas dos acompanhantes. Na terceira etapa, iniciou-se a elaboração textual. Na quarta etapa, houve a captação de modelos, seleção e elaboração de 38 ilustrações. A quinta etapa correspondeu à diagramação do manual, a qual foi realizada de acordo com as recomendações da NBR6029 e desenvolvida através do programa CorelDraw 15.0. Realizadas as cinco etapas de construção do manual educativo, passou-se para o processo de validação da tecnologia educativa produzida. Na sexta etapa, foram convidados, de acordo com critérios pré-estabelecidos, nove especialistas na área de interesse (saúde da mulher; obstetrícia; tecnologia em saúde; e validação de instrumentos), os quais avaliaram objetivos, estrutura, apresentação e relevância do manual. Um determinado item foi considerado validado quando o mesmo obteve a classificação de “Totalmente Adequado” por pelo menos metade mais um do número de especialistas e Índice de Validade de Conteúdo (IVC) maior ou igual a 0,78. Alguns itens foram satisfatoriamente avaliados e outros necessitaram de modificações. Quantos aos objetivos do manual, os especialistas consideraram validados todos os itens questionados, tendo o IVC variado entre 0,88 e 1,0. Quanto a estrutura e apresentação do manual, três itens necessitaram adequar-se as sugestões dos especialistas: clareza e objetividade das mensagens; sequência lógica do conteúdo e correspondências do estilo da redação ao nível de conhecimento do público-alvo. O IVC dos itens pertencentes a este tópico variou entre 0,66 e 1,0. Todos os itens referentes à relevância do manual foram considerados validados, tendo o IVC variado entre 0,88 e 1,0. O IVC Global do manual educativo foi de 0,94. Na sétima etapa, o manual educativo foi aplicado junto a onze representantes do público-alvo, os quais tiveram nível de concordância acima de 75% nos itens referentes à organização, estilo da escrita, aparência e motivação do manual. Na oitava etapa, foram realizadas as alterações sugeridas por especialistas e representantes do público-alvo: reformulação de frases; substituição de palavras ou expressões; inclusão, substituição ou realocação de informações e ilustrações. A nona etapa correspondeu à revisão de português por profissional especializado. Na décima etapa, foi verificado o Índice de Legibilidade de Flesch (ILF). Os tópicos do manual tiveram ILF entre 50 e 94, o que corresponde a uma leitura “Muito Fácil” ou “Fácil”, adequada a um público com até nove anos de estudo. A última etapa correspondeu ao encaminhamento para impressão. Por fim, considera-se o manual educativo validado por especialistas e representantes do público-alvo quanto à sua aparência e conteúdo, sendo necessário estudo posterior para a avaliação do impacto desta tecnologia sobre a postura do acompanhante em sala de parto.

OLIVEIRA, Amanda Souza de. Análise de influência do apoio prestado pelo acompanhante em sala de parto na satisfação e resultados maternos e neonatais de primíparas. 2014. 81 f. Dissertação (Mestrado em Enfermagem) - Universidade Federal do Ceará. Faculdade de Farmácia, Odontologia e Enfermagem, Fortaleza, 2014. / Submitted by denise santos (denise.santos@ufc.br) on 2014-07-25T15:23:38Z No. of bitstreams: 1 2014_dis_asoliveira.pdf: 1210007 bytes, checksum: de78c9c883af3be4039e14f3d771da6b (MD5) / Approved for entry into archive by denise santos(denise.santos@ufc.br) on 2014-07-25T15:24:02Z (GMT) No. of bitstreams: 1 2014_dis_asoliveira.pdf: 1210007 bytes, checksum: de78c9c883af3be4039e14f3d771da6b (MD5) / Made available in DSpace on 2014-07-25T15:24:02Z (GMT). No. of bitstreams: 1 2014_dis_asoliveira.pdf: 1210007 bytes, checksum: de78c9c883af3be4039e14f3d771da6b (MD5) Previous issue date: 2014 / Introdução: O cuidado prestado à mulher durante o processo de nascimento vem passando por mudanças com vistas à humanização da assistência. Neste sentido, salta aos olhos à atual assistência oferecida à mulher, marcada pela medicalização e dominação do corpo, em detrimento do respeito ao fenômeno natural e fisiológico do parto. O processo de nascimento consiste em momento frágil e vulnerável, tornando imprescindível a participação do acompanhante no processo parturitivo.Objetivos: Analisar a influência do apoio prestado pelo acompanhante na satisfação de primíparas e nas variáveis do processo de parto e sobre os resultados maternos e neonatais, comparar os resultados maternos e neonatais acerca dos eventos do trabalho de parto e parto entre os grupos caso (com apoio por acompanhante de sua escolha) e controle (sem acompanhante) e comparar a satisfação da parturiente com a experiência do trabalho de parto e parto entre o grupo de caso e o grupo-controle. Metodologia: O estudo foi do tipo caso-controle, realizado com puérperas primíparas internadas no período de maio a outubro de 2013 no alojamento conjunto da Maternidade Escola Assis Chateaubriand. O grupo caso foram puérperas primíparas internadas que receberam acompanhante durante o parto e que não receberam apoio durante o parto por doulas. O grupo controle foram puérperas primíparas que não receberam acompanhante durante a sala de parto. A coleta de dados foi realizada através de formulário estruturado e formulários organizados no método auto-relato, que foram previamente testados com parturientes, e reformulados após avaliação. Foram incluídos na amostra 50 controles e 100 casos (total de 150 puérperas). Os dados foram analisados no programa estatístico SPSS, utilizando os testes adequados. O projeto foi aprovado pelo Comitê de Ética em pesquisa da Maternidade Escola Assis Chateaubriand, segundo parecer de nº 253671. Resultados: A amostra consta de 150 puérperas, das quais tinham uma idade média de 23 anos, a maioria estava entre 20 e 29 anos (64; 42,7%), era proveniente da capital (105; 70,0%), eram casadas/união estável (100; 66,7%), com renda familiar de 1 a 2 salários mínimos (60; 40,0%) e tinham até 8 anos de estudo (67; 44,7%). Observou-se que a maioria das parturientes respondeu que o apoio do acompanhante foi muito importante (53,0%) tanto no trabalho de parto quanto tanto durante o parto (45,0%), a ajuda do companheiro foi bastante útil tanto no trabalho de parto (65,0%) quanto no parto (66,0%). A presença do acompanhante em sala de parto foi estatisticamente significante nas seguintes variáveis: a presença de um acompanhante durante a assistência pré-natal (p=0,05), a duração média do trabalho de parto das gestantes (p=0,01), a realização de anestesia epidural (p=0,01), a dor sentida durante o trabalho de parto (p=0,001) e parto(p=0,01), a confiança durante o trabalho de parto (p= 0,001) e parto(p = 0,001), o medo durante o trabalho de parto (p = 0,001), as expectativas da dor durante o trabalho de parto (p= 0,01) e parto (p= 0,02). Conclusão: O apoio por acompanhante escolhido pela parturiente associou-se a maior satisfação global das parturientes com a experiência do nascimento. Verifica-se, portanto, a importância de garantir o direito de participação do acompanhante durante o trabalho de parto e parto, respeitando assim a escolha de cada mulher durante o processo parturitivo.

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico. Programa de Pós-Graduação em Ciência da Computação. / Made available in DSpace on 2012-10-21T14:51:24Z (GMT). No. of bitstreams: 1 206927.pdf: 1257800 bytes, checksum: 238446807652ab06b7b697c57995ce56 (MD5) / A Robótica Baseada em Comportamentos (RBC) se baseia na emergência de comportamentos robóticos de modo a garantir inteligência e autonomia nas ações que um agente deve descrever para alcançar seus objetivos. Desta forma, surge a necessidade de se achar uma maneira formal de representar estes comportamentos robóticos, mantendo características como complexidade, concisão e compactação na representação. Neste trabalho se afirma que as linguagens contidas na hierarquia de Chomsky são capazes de representar esta variada gama de comportamentos robóticos.

Dissertação (mestrado)—Universidade de Brasília, Institudo de Ciências Exatas, Departamento de Ciência da Computação, 2014. / Submitted by Albânia Cézar de Melo (albania@bce.unb.br) on 2014-10-21T13:01:44Z No. of bitstreams: 1 2014_ArianeAlvesAlmeida.pdf: 1238432 bytes, checksum: 443ba143f22122e23f5542311f804fe9 (MD5) / Approved for entry into archive by Tania Milca Carvalho Malheiros(tania@bce.unb.br) on 2014-10-22T15:32:03Z (GMT) No. of bitstreams: 1 2014_ArianeAlvesAlmeida.pdf: 1238432 bytes, checksum: 443ba143f22122e23f5542311f804fe9 (MD5) / Made available in DSpace on 2014-10-22T15:32:03Z (GMT). No. of bitstreams: 1 2014_ArianeAlvesAlmeida.pdf: 1238432 bytes, checksum: 443ba143f22122e23f5542311f804fe9 (MD5) / Uma abordagem é apresentada para verificar formalmente a corretude lógica de operadores algébricos implementados em hardware. O processo de verificação é colocado em paralelo ao fluxo convencional de projeto de hardware, permitindo a verificação de fragmentos da implementação do hardware tanto simultaneamente quanto após todo o processo de implementação ser concluído, evitando assim atrasos no projeto do circuito. A ideia principal para atestar a corretude de uma implementação em hardware é comparar seu comportamento operacional com uma definição formal de seu operador, analisando assim sua equivalência funcional; isto é, se ambas definições, de hardware e matemática, produzem os mesmos resultados quando fornecidas as mesmas entradas. A formalização dessa comparação é um desafio desta abordagem, já que as provas utilizadas para verificar a corretude e outras propriedades desses sistemas pode seguir esquemas indutivos, que proveem de maneira natural quando se trata com definições recursivas, usadas em linguagens de especificação e ferramentas de formalização. Já que Linguagens de Descrição de Hardware descrevem circuitos/sistemas de maneira imperativa, a abordagem se baseia na tradução conservativa de comandos iterativos presentes nessas linguagens em suas respectivas especificações recursivas. Esses esquemas de provas indutivas são baseados em garantir pré e pós-condições, bem como a preservação de invariantes durante todos os passos da execução recursiva, de acordo com a abordagem da lógica de Floyd-Hoare para verificação de procedimentos imperativos. A aplicabilidade da metodologia é ilustrada com um caso de estudo utilizando o assistente de prova de ordem superior PVS para fornecer prova de correção lógica de uma implementação em FPGA do algoritmo para inversão de matrizes de Gauss-Jordan (GJ). Essas provas em PVS são dadas em um estilo dedutivo baseado no Cálculo de Gentzen, aproveitando facilidades desse assistente, como tipos dependentes, indução na estrutura de tipos de dados abstratos e, é claro, suas linguagens de especificação e prova em lógica de ordem superior. ________________________________________________________________________________ ABSTRACT / An approach is introduced to formally verify the logical correctness of hardware implementations of algebraic operators. The formal verification process is placed sidelong the usual hardware design flow, allowing verification on fragments of the hardware implementation either simultaneously or after the whole implementation process finished, avoiding in this way hardware development delays. The main idea to state the correctness of a hardware implementation, is to compare its operational behavior with a formal definition of the operator, analysing their functional equivalence; that is, if both the hardware and the mathematical definition produce the same results when provided with the same entries. The formalization of this comparison is a challenge for this approach, since the proofs used to verify soundness and other properties of these systems might follow inductive schemata, that arise in a natural manner when dealing with recursive definitions, used in specifications languages of formalization tools. Since Hardware Description Languages describe circuits/systems in an imperative style, the approach is based on a conservative translation of iterative commands into their corresponding recursive specifications. The inductive proof schemata are then based on guaranteeing pre and post-conditions as well as the preservation of invariants during all steps of the recursive execution according to the Floyd-Hoare’s logical approach for verification of imperative procedures. The applicability of the methodology is illustrated with a case study using the higher-order proof assistant PVS by proving the logical correction of an FPGA implementation of the Gauss-Jordan matrix inversion algorithm (GJ). These PVS proofs are given in a Gentzen based deductive style taking advantage of nice features of this proof assistant such as dependent types and induction in the structure of abstract data types, and, of course, of its higher-order specification and proof languages.

Submitted by Ricardo Carrasco (ricardogc84@uepb.edu.br) on 2016-10-25T11:59:05Z No. of bitstreams: 1 PDF - Maria Aparecida Calado de Oliveira Dantas.pdf: 43705106 bytes, checksum: 936e8c0fbd4d45243311a5a3cc13c62f (MD5) / Approved for entry into archive by Irenilda Medeiros (nildamedeiros@uepb.edu.br) on 2016-11-07T19:31:35Z (GMT) No. of bitstreams: 1 PDF - Maria Aparecida Calado de Oliveira Dantas.pdf: 43705106 bytes, checksum: 936e8c0fbd4d45243311a5a3cc13c62f (MD5) / Made available in DSpace on 2016-11-07T19:31:35Z (GMT). No. of bitstreams: 1 PDF - Maria Aparecida Calado de Oliveira Dantas.pdf: 43705106 bytes, checksum: 936e8c0fbd4d45243311a5a3cc13c62f (MD5) Previous issue date: 2015-03-25 / It is a fact that the school seems to ignore the importance of developing a work outlined in the actual social practices of individuals, despite the efforts of government programs to promote significant improvements to the process of teaching and learning the mother tongue. In this sense, the work aims to discuss the space of orality in the Portuguese language classes and enable an intervention proposal based on work with oral genres, focusing on student speech, comprising the oral language as interactive practice / information. For the development of research, it was investigated the teacher's pedagogic practice in their teaching action on the elementary school in Municipal Elementary School Nossa Senhora do Rosario- Pombal - PB, and the adoption of questionnaires and interviews (semi-structured) which allowed us to ask the teacher about their training and classroom practices, the answers possibility to observe oral concepts, language and adopted language to later propose a reflection on the relevance of the work with the oral genres in school. Also there was the treatment of oral genres by textbooks mother tongue, adopted by the field school research, paying attention to the theoretical perspectives that guide this material to support the development of pedagogical practices of the teacher of mother tongue. Finally, teaching action proposal was presented that would allow one to contemplate aspects of orality in language teaching, deemed relevant by official documents and theoretical postulates underlying the treatment of tongue (gem) today. The study was supported by theorists of contemporary linguistics engaged in research work with the textual genres, oral and written, in the classroom of mother tongue, such as Marcuschi (2003), Mollica (2011), Rojo (2010), Elias (2011), Bortoni-Ricardo (2009), Signorini (2001), Matencio (2001) and Dolz & Schneuwly (2001), among other authors who stress the importance of working with orality in school learning. Thus, the research fits the role of qualitative studies in the Graduate Programs nationwide Teacher Training, is based on the National Curriculum Parameters (BRAZIL, NCP, 1998), which present a focused attention to the practical orality in elementary school, little explored by making teaching and textbooks of the Portuguese language, as shown in the study focus, and points to the view that it is possible to develop a methodology that addresses the systematization of the formal oral genres in mother tongue classes . / É fato que a escola parece ignorar a relevância de se desenvolver um trabalho pautado nas reais práticas sociais dos indivíduos, apesar do empenho de programas governamentais em promover melhorias significativas para o processo de ensino e aprendizagem da língua materna. Neste sentido, o trabalho tem o objetivo de discutir o espaço da oralidade nas aulas de língua portuguesa e viabilizar uma proposta de intervenção fundamentada no trabalho com os gêneros textuais orais, com foco na fala do aluno, compreendendo a linguagem oral como prática interativa/informativa. Para o desenvolvimento da pesquisa, investigou-se a prática pedagógica do professor em sua ação docente frente ao Ensino Fundamental na Escola Municipal de Ensino Fundamental Nossa Senhora do Rosário – Pombal – PB, além da adoção de questionário e entrevista (semiestruturada) que nos permitiu interrogar o docente sobre sua formação profissional e práticas de sala de aula, cujas respostas possibilitaram verificar concepções de oralidade, língua e linguagem adotadas, para posteriormente propor uma reflexão sobre a relevância do trabalho com os gêneros orais na escola. Também verificou-se o tratamento dado aos gêneros orais pelos livros didáticos de língua materna, adotados pela escola campo da pesquisa, atentando para as correntes teóricas que norteiam esse material de apoio ao desenvolvimento das práticas pedagógicas do professor de língua materna. Finalmente, foi apresentada uma proposta de ação docente que permitisse contemplar aspectos da oralidade no ensino de língua, considerados relevantes pelos documentos oficiais e postulados teóricos que fundamentam o tratamento da língua(gem) na atualidade. O estudo esteve apoiado por teóricos da linguística contemporânea que se dedicam a investigação do trabalho com os gêneros textuais, orais e escritos, na sala de aula de língua materna, tais como Marcuschi (2003), Mollica (2011), Rojo (2010), Elias (2011), Bortoni-Ricardo (2009), Signorini (2001), Matencio (2001) e Schneuwly & Dolz (2001), dentre outros teóricos que ressaltam a importância do trabalho com a oralidade na aprendizagem escolar. Dessa forma, a pesquisa se inscreve no rol dos estudos qualitativos realizados em Programas de PósGraduação em Formação de Professores de âmbito nacional, se fundamenta nos Parâmetros Curriculares Nacionais (BRASIL, PCN, 1998), os quais apresentam uma atenção voltada para as práticas da oralidade no Ensino Fundamental, pouco exploradas pelo fazer docente e livros didáticos de língua portuguesa, conforme demonstra o estudo em foco, e aponta para a perspectiva de que é possível desenvolver uma metodologia que contemple a sistematização dos gêneros orais formais nas aulas de língua materna.

nÃo hà / Long running applications are very common in High Performance Computing (HPC) domains. During the execution of this kind of application, some improvements or corrections can be identified and applied without making invalid the data that has been processed. In these cases, the ability to make changes in a parallel program during execution is considered useful. Dynamic reconfiguration is the term used to describe this technique, which can be implemented using different alternatives, like architecture description languages (ADL). An ADL allows a the specification of a software based on exogenous conectors to combine and define data types and protocols for orchestrating the interaction between components. This research has the goal of designing an ADL and implementing a configuration interpretation environment for the HPE component-based parallel computing platform. The main purpose of this language is to provide the ability to specify exogenous connectors and support dynamic reconfiguration. Case studies evaluate the performance of the component interpretation developed by the ADL, as well as validate the actions of dynamic reconfiguration. The results are an evidence that the overhead in the interpretation process for realistic problem instances is acceptable, in such a way that, when used wisely, the connectors can be used even in production scenarios. In some cases, the interpretation weight can be disregarded. The reconfiguration experiments are also deemed satisfactory, making the simplicity of the mechanism the major draw of the solution. / Nos domÃnios da ComputaÃÃo de Alto Desempenho (CAD), sÃo comuns aplicaÃÃes com tempo de execuÃÃo de longa duraÃÃo. Durante a execuÃÃo de uma aplicaÃÃo dessa natureza, podem ser identificadas melhorias ou correÃÃes nos algoritmos em execuÃÃo que nÃo invalidam o processamento previamente realizado. Neste cenÃrio, a capacidade de realizar modificaÃÃes em tempo de execuÃÃo se mostra de grande utilidade. A esta tÃcnica chamamos reconfiguraÃÃo dinÃmica, a qual, dentre outros meios discutidos ao longo do trabalho, pode ser implementada a partir do uso de linguagens de propÃsito especÃfico como as linguagens de descriÃÃo de arquitetura (ADL). Uma ADL permite a especificaÃÃo de um sistema de software a partir da construÃÃo de conectores exÃgenos com a funÃÃo de combinar e definir os formatos de dados e protocolos nas interaÃÃes de componentes. Este trabalho de pesquisa tem como objeto o projeto de uma ADL e a implementaÃÃo de um ambiente de interpretaÃÃo de configuraÃÃo para a plataforma de componentes paralelos HPE (Hash Programming Environment). Essa linguagem tem como principal propÃsito oferecer a capacidade de especificar conectores exÃgenos e suporte à reconfiguraÃÃo dinÃmica. Estudos de caso avaliam o desempenho da interpretaÃÃo dos componentes desenvolvidos pela ADL, como tambÃm validam as operaÃÃes de reconfiguraÃÃo dinÃmica. Os resultados mostram sobrecarga considerada aceitÃvel no processo de interpretaÃÃo, para instÃncias realÃsticas de problemas, de forma que, quando utilizado com prudÃncia, os conectores podem ser utilizados atà mesmo em cenÃrios de produÃÃo. Em alguns casos, o peso da interpretaÃÃo chega a ser desprezÃvel. Os ensaios de reconfiguraÃÃo tambÃm se mostram satisfatÃrios para os requisitos apresentados, sendo um dos principais diferencias da soluÃÃo, a simplicidade de uso do mecanismo.

Made available in DSpace on 2014-06-12T16:01:17Z (GMT). No. of bitstreams: 2 arquivo7289_1.pdf: 2013918 bytes, checksum: e3f26e432c831b7c299664b62269fd01 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2005 / Petróleo Brasileiro S.A. / Como outros métodos visuais orientados a objetos, UML tem influenciado tremendamente a prática de modelagem na engenharia de software com ricos mecanismos de estruturação. Porém, apesar de suas vantagens e adoção em larga escala, na prática, a falta de uma semântica formal tem dificultado o desenvolvimento rigoroso baseado em modelos de aplicações não triviais (aplicações que por sua natureza necessitam de ênfase na especificação e na verificação de seus componentes). A razão para isto é que transformações de modelos podem não preservar a semântica e, como conseqüência, o comportamento do modelo. Este problema é ainda mais sério em transformações que envolvem diferentes visões do modelo. Limitações similares podem ser encontradas durante o desenvolvimento com UML-RT. Esta linguagem é uma extensão conservativa de UML que provê a noção de objetos ativos (objetos com um comportamento próprio, independente do fluxo de execução do restante do sistema) para descrever aplicações concorrentes e distribuídas. Neste tipo de desenvolvimento, transformações devem lidar simultaneamente com as diferentes visões estáticas e dinâmicas do modelo, representadas por seus diagramas e propriedades. Por estes motivos, este trabalho propõe uma semântica para UML-RT, mapeando suas construções em OhCircus, uma linguagem formal, orientada a objetos, que combina CSP e Z, e que suporta o cálculo de refinamentos de Morgan. A partir desta semântica, bem como das noções e leis de refinamentos de OhCircus, é possível propor leis de transformação de modelos passíveis de demonstração e que preservam o comportamento do sistema. Estas leis de transformação são propostas em duas categorias: a primeira delas é um conjunto abrangente de leis básicas que expressam pequenas mudanças nas principais visões do modelo, como a declaração ou remoção de elementos do modelo; já a segunda representa leis de transformação de maior granularidade, derivadas a partir da composição de leis básicas, como a decomposição de uma cápsulas em cápsulas operando em paralelo. Tais transformações derivadas podem ser vistas como refatoramentos (refactorings) corretos sobre o modelo, facilmente aplicáveis durante um processo de desenvolvimento rigoroso, sem que o desenvolvedor tenha conhecimento do formalismo que o suporta. Finalmente, a abrangência deste conjunto de leis é discutida particularmente através dos principais passos de uma estratégia de redução de modelos UML-RT a um modelo UML estendido com um único objeto ativo, responsável por todas as interações com o ambiente e por conservar o comportamento dinâmico do sistema modelado. Este modelo UML estendido pode ser visto como uma forma normal, e, portanto, nossa estratégia pode ser vista como uma contribuição para uma estratégia mais global de completude capturada por redução a esta forma normal

Made available in DSpace on 2014-06-12T16:28:11Z (GMT). No. of bitstreams: 5 arquivo2317_1.pdf: 6104975 bytes, checksum: 6e3fc6e8d8267bcaa1935c38062220a9 (MD5) arquivo2317_2.pdf: 10078757 bytes, checksum: 4c994be1fc019742fddcb561687eb7c4 (MD5) arquivo2317_3.pdf: 9649486 bytes, checksum: 051f487fd78f8977016293ea7e177bdc (MD5) arquivo2317_4.pdf: 4283654 bytes, checksum: 4d87fedf7fb1f5aa5806a38c86a837ff (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2008 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / Esta dissertação de mestrado tem como objetivo identificar padrões formais que caracterizem tipologias de cabeceiras de pontes no decorrer do processo histórico de formação urbana de cidades atravessadas pelas águas. Neste intuito, adota como estudo de caso a composição formal das cabeceiras das pontes do centro da cidade do Recife, durante quatro séculos de sua história (XVII-XX). Isto, devido ao fato de esta constituir um exemplar de cidade cujo núcleo original atravessado pelas águas exigiu a construção de sucessivas pontes para viabilizar a sua expansão rumo ao continente. Já as cabeceiras das pontes de seu centro histórico, configuram estudos de casos representativos quanto à incidência de práticas urbanísticas que conduziram a uma série de variações formais ao longo de sua história. Para tanto, a pesquisa centra-se no tema de leitura da forma urbana, referenciando-se, teoricamente, nos campos da morfologia e da história urbana, através de autores tais como: Lamas (2000), Aumont (1990), Rossi (1966), Argan (2000), Caniggia & Maffei (1995), Poète (1929), De Quincy (1977), Sitte (1889) e Krier (1979). Neste sentido, a dissertação utiliza como conceitos-chave, os termos: padrões formais - aspecto multiplicador do método analítico - e tipologias espaciais urbanas - aspecto sintetizador do método analítico. Deste modo, tem como finalidade contribuir para a teoria da morfologia urbana, através da caracterização de mais uma tipologia espacial urbana - a cabeceira de ponte -, assim como através do emprego de métodos de leitura da forma urbana. Na medida em que o estudo de caso incide sobre as cabeceiras de pontes do centro da cidade do Recife, esta pesquisa visa contribuir, também, para a história urbana desta cidade. Como conclusão, a pesquisa identifica uma série de padrões formais que caracteriza as variações das composições formais das cabeceiras das pontes do centro da cidade do Recife, bem como aponta para algumas tipologias espaciais urbanas de cabeceiras de pontes de cidades atravessadas pelas águas

Orientador: Walter Alexandre Carnielli / Tese (doutorado) - Universidade Estadual de Campinas, Instituto de Filosofia e Ciencias Humanas / Made available in DSpace on 2018-07-27T00:20:42Z (GMT). No. of bitstreams: 1 Gracio_MariaClaudiaCabrini_D.pdf: 5288226 bytes, checksum: 9167acf60882f6defde6670ad61fb1e8 (MD5) Previous issue date: 1999 / Resumo: Este trabalho introduz uma ampla família de extensões monotônicas da lógica de primeira ordem, denominada lógicas moduladas, construída estendendo a lógica clássica por meio de quantificadores generalizados, chamados quantificadores modulados. Tais quantificadores representam várias formas de raciocínio indutivo. Alguns resultados gerais em teoria de modelos para esta família são também obtidos. Particularmente, propõem-se três sistemas lógicos monotônicos, os quais formalizam conjuntos indutivos de crenças em bases de conhecimento, gerados por argumentos indutivos das formas "a maioria", "muitos" e "para uma 'boa' parte". A noção de "maioria" é capturada por meio de um -quantificador modulado, semanticamente interpretado pelos números cardinais dos conjuntos de evidências. É mostrado que este sistema, embora seja correto, não é completo com relação ao modelo definido. A fim de capturar a noção de "muitos" e "para uma 'boa' parte" novos quantificadores modulados são introduzidos, semanticamente interpretados, respectivamente, pelas noções de família fechada superiormente e topologia reduzida. Demonstra-se que ambos os sistemas são extensões conservativas da lógica clássica que preservam importantes propriedades, como correção e completude. O trabalho também discute outras perspectivas e inclui alguns problemas em aberto e questões / Abstract: This work introduces a large family of monotonic extensions of first order logic denominated modulated logics, constructed by extending classical logic through generalized quantifiers called modulated quantifiers. Such quantifiers represent various forms of inductive reasoning. Some general results in model theory for this family are also obtained. Particularly, it proposes three monotonic logical systems, which formalize inductive sets of beliefs in knowledge bases generated by inductive arguments of the form "most", "many" and "for a 'good' number of. The notion af "most" is captured by means of a modulated quantifier semantically interpreted by cardinal numbers in sets of evidences. It is proven that this system, although sound, is not complete if checked against the intended model. In order to capture the notion of "many" and "for a 'good' number of new modulated quantifiers are introduced, semantically interpreted, respectively, by the notions of upperly closed family and reduced topology. It proves that both systems are conservative extensions of classical logic preserving important properties, like soundness and completeness. The work also discusses further perspectives and includes several open problems and questions / Doutorado / Doutor em Filosofia

Orientador: Walter Alexandre Carnielli / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Filosofia e Ciencias Humanas / Made available in DSpace on 2018-07-28T15:09:20Z (GMT). No. of bitstreams: 1 Almeida_JoaoMarcosde_M.pdf: 7102559 bytes, checksum: 00cfc40892f4fb1bb2cc560c907a732b (MD5) Previous issue date: 1999 / Mestrado