Submitted by Diogo Barreiros (diogo.barreiros@ufba.br) on 2017-02-17T16:37:53Z No. of bitstreams: 1 barboza2006.pdf: 716139 bytes, checksum: 56397fad812dffadf11ce4841ed6c59c (MD5) / Approved for entry into archive by Vanessa Reis (vanessa.jamile@ufba.br) on 2017-02-21T11:53:04Z (GMT) No. of bitstreams: 1 barboza2006.pdf: 716139 bytes, checksum: 56397fad812dffadf11ce4841ed6c59c (MD5) / Made available in DSpace on 2017-02-21T11:53:04Z (GMT). No. of bitstreams: 1 barboza2006.pdf: 716139 bytes, checksum: 56397fad812dffadf11ce4841ed6c59c (MD5) / O termo IEEE 802.11 diz respeito a uma família de especificações que buscam obter conectividade sem fio para estações fixas, portáveis e móveis em uma rede local. Redes IEEE 802.11 têm, recentemente, despertado interesse como tecnologia de suporte para a comunicação em aplicações sem fio na automação, em particular em aplicações de chão de fábrica e de controle de plantas, onde, muitas vezes, requisitos de tempo-real e requisitos de confiabilidade são necessários. Neste contexto, o uso de métodos formais permite a obtenção de um conhecimento mais preciso sobre as propriedades do protocolo bem como a especificação e verificação destas propriedades. Este trabalho apresenta uma especificação e verificação formal da função de controle de acesso ao meio da sub-camada MAC do padrão IEEE 802.11 usando UPPAAL, um verificador de modelos gratuito, que suporta os conceitos de relógios e tempo. O uso do UPPAAL permitiu considerar, dentro da modelagem, as características temporais do protocolo. A verificação procurou identificar uma série de propriedades que fornecesse aos projetistas de aplicações e sistemas de tempo-real um conjunto mínimo de garantias relativas aos canais de comunicação. Entre as propriedades verificadas, destacamos a habilidade das estações possuírem acesso ao meio dentro de um tempo finito e conhecido e, portanto, a adequação do protocolo como suporte a aplicações que necessitem de garantias temporais.

SALES, Juliano Efson Norberto. Coordenação e reconfiguração dinâmica de componentes em uma plataforma de computação paralela. 2012. 144 f. Dissertação (Mestrado em ciência da computação)- Universidade Federal do Ceará, Fortaleza-CE, 2012. / Submitted by Elineudson Ribeiro (elineudsonr@gmail.com) on 2016-07-11T17:31:37Z No. of bitstreams: 1 2012_dis_jensales.pdf: 3112116 bytes, checksum: e6dad36307eb52f19a718046ca764535 (MD5) / Approved for entry into archive by Rocilda Sales (rocilda@ufc.br) on 2016-07-18T15:42:23Z (GMT) No. of bitstreams: 1 2012_dis_jensales.pdf: 3112116 bytes, checksum: e6dad36307eb52f19a718046ca764535 (MD5) / Made available in DSpace on 2016-07-18T15:42:23Z (GMT). No. of bitstreams: 1 2012_dis_jensales.pdf: 3112116 bytes, checksum: e6dad36307eb52f19a718046ca764535 (MD5) Previous issue date: 2012 / 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.

MARCILON, Thiago Braga. Contratos formais para derivação e verificação de componentes paralelos. 2012. 156 f. Dissertação (Mestrado em ciência da computação)- Universidade Federal do Ceará, Fortaleza-CE, 2012. / Submitted by Elineudson Ribeiro (elineudsonr@gmail.com) on 2016-07-12T18:10:13Z No. of bitstreams: 1 2012_dis_tbmarcilon.pdf: 1474623 bytes, checksum: e61fb07d3a835088ff5a53d4eb684f2d (MD5) / Approved for entry into archive by Rocilda Sales (rocilda@ufc.br) on 2016-07-22T12:39:34Z (GMT) No. of bitstreams: 1 2012_dis_tbmarcilon.pdf: 1474623 bytes, checksum: e61fb07d3a835088ff5a53d4eb684f2d (MD5) / Made available in DSpace on 2016-07-22T12:39:34Z (GMT). No. of bitstreams: 1 2012_dis_tbmarcilon.pdf: 1474623 bytes, checksum: e61fb07d3a835088ff5a53d4eb684f2d (MD5) Previous issue date: 2012 / The use of cloud computing to offer High Performance Computing (HPC) services has been widely discussed in the academia and industry. In this respect, this dissertation is included in the context of designing a cloud computing platform for the development of component-based parallel computing applications, referred as cloud of components. Many important challenges about using the cloud of components relate to parallel programming, an error-prone task due to synchronization issues, which may lead to abortion and production of incorrect data during execution of applications, and the inefficient use of computational resources. These problems may be very relevant in the case of long running applications with tight timelines to obtain critical results, quite common in the context of HPC. One possible solution to these problems is the formal analysis of the behavior of the components of an application through the cloud services, before their execution. Thus, the users of the components may know if a component can be safely used in their application. In this scenario, formal methods becomes useful. In this dissertation, it is proposed a process for specification and derivation of parallel components implementation for the cloud of components. This process involves the formal specification of the components behavior through contracts described using the Circus formal specification language. Then, through a refinement and translation process, which takes the contract as a start point, one may produce an implementation of a component that may execute on a parallel computing platform. Through this process, it becomes possible to offer guarantees to developers about the components behavior in their applications. To validate the proposed idea, the process is applied to contracts that have been described based on two benchmarks belonging to the NAS Parallel Benchmarks, widely adopted in HPC for evaluate the performance of parallel programming and computing platforms. / A aplicação de nuvens computacionais para oferecer serviços de Computação de Alto Desempenho (CAD) é um assunto bastante discutido no meio acadêmico e industrial. Esta dissertação está inserida no contexto do projeto de uma nuvem computacional para o desenvolvimento e execução de aplicações de CAD baseadas em componentes paralelos, doravante denominada nuvem de componentes. Um dos principais desafios na sua utilização consiste no suporte à programação paralela, tarefa bastante suscetível à erros, pois tais erros podem levar, ao longo do desenvolvimento, a problemas de sincronização de processos, que podem causar abortamento da execução e a produção de dados incorretos, bem como a problemas relacionados ao uso ineficiente dos recursos computacionais. É importante que tais problemas sejam tratados no caso de aplicações de longa duração cujo respeito a um cronograma para obtenção de resultados é crítico, aplicações estas bastante comuns no contexto de CAD. Uma possível solução para tais problemas consiste na verificação do comportamento e das propriedades dos componentes na nuvem, antes que seja feita a sua execução, tornando possível que os usuários dos componentes da nuvem saibam se um componente pode ser utilizado com segurança em sua aplicação. Nesse cenário, o uso de métodos formais surge como uma alternativa atraente. A contribuição desta dissertação consiste em um processo de derivação e verificação de propriedades de componentes na nuvem. Tal processo envolve a especificação formal do comportamento dos componentes por meio de contratos descritos pela linguagem Circus. Então, através de um processo de refinamento e tradução tendo como ponto de partida o contrato, chega-se à implementação de um componente para execução sobre uma plataforma de computação paralela. Através desse processo, torna-se possível oferecer garantias aos desenvolvedores em relação ao comportamento dos componentes no contexto de suas aplicações. Para a prova de conceito, o processo é aplicado sobre a especificação "papel-e-caneta" de dois benchmarks do NAS Parallel Benchmarks, IS e CG, bastante difundidos na área de CAD.

Made available in DSpace on 2012-09-06T01:11:19Z (GMT). No. of bitstreams: 2 license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) 928.pdf: 1109397 bytes, checksum: c2bf4e1a3bf0db29fbf4bc9ccfafaa33 (MD5) Previous issue date: 2007 / (...) Os conselhos gestores de políticas públicas surgem como canais institucionalizados de participação e ocuparam espaço na implementação de um novo padrão de políticas sociais, incluindo as políticas sociais voltadas às questões da pobreza, embora venham enfrentando dificuldades para garantir a democratização na sociedade. O Programa de Transferência de Renda Condicionada Bolsa Família (PBF) criado em outubro de 2003 torna-se uma iniciativa capaz de iluminar os impasses e dilemas envolvidos na consolidação de estratégias de combate à pobreza. O controle e participação social do Programa devem ser realizados em âmbito local, respeitada a paridade entre governo e sociedade. A montagem e a execução de um sistema de monitoramento e avaliação do PBF, bem como de divulgação dessas informações, serão instrumentos essenciais para o exercício do controle público, entendido como o exercício do controle sobre as políticas por parte dos representantes do governo e da sociedade civil. Neste estudo, a perspectiva é investigar, através da experiência local de Duque de Caxias, como se desenvolve o controle social no PBF a partir do que é previsto em sua criação, como a formação de conselhos gestores ou comitês participativos, do que está sendo redefinido no nível federal para o papel destas instâncias de participação social em meio ao processo de implementação e como estas questões estão sendo equacionadas, em meio à legitimação destes espaços de controle social em um contexto vivo de participação social e às relações políticas marcadas pelo populismo e clientelismo. (...) A abertura de espaços para a participação da sociedade na gestão do PBF, ainda que indispensáveis, não foram suficientes para a efetivação da participação. Torna-se necessário uma maior integração entre as diferentes instâncias locais envolvidas na implementação e execução do PBF, com capacidade técnica de intervenção e garantia da participação social em todo o processo.

Made available in DSpace on 2016-03-04T13:55:11Z (GMT). No. of bitstreams: 2 4.pdf: 1725584 bytes, checksum: 95e2e35ced41be5b57d848564e502b68 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2014 / Fundação Oswaldo Cruz. Instituto de Tecnologia em Fármacos/Farmanguinhos. Rio de Janeiro, RJ, Brasil. / A nanotecnologia é uma tecnologia transdisciplinar que está sendo desenvolvida e aplicada em diversas áreas, dentre as quais cabe ressaltar a da saúde, principalmente no que tange à terapêutica e ao diagnóstico. Na oncologia os tratamentos são muito prolongados, a necessidade de exames de imagem é frequente, as doses administradas dos tratamentos são muito elevadas e a toxicidade para o paciente é, muitas vezes, o fator limitante da terapia. Com os avanços da nanotecnologia, espera-se que essas deficiências sejam resolvidas ou, pelo menos, amenizadas, tendo em vista algumas características especiais destes materiais. Entretanto, ainda não se tem clara a relação entre essas características e seus efeitos toxicológicos. Por isso, é necessário entender se os requisitos regulatórios, em termos de avaliação toxicológica, para registro de um medicamento com base em nanotecnologia, são capazes de identificar os possíveis riscos advindos desta nova tecnologia. Esse trabalho teve por objetivo comparar a abordagem regulatória da EMA, FDA e ANVISA com relação à avaliação de nanomedicamentos em comparação com medicamentos convencionais. Para isso, foi analisado o perfil toxicológico do DOXIL® em relação a doxorrubicina convencional. Esse medicamento foi escolhido para ser analisado por ser o primeiro lipossoma aprovado pelo FDA, em 1995, e pela importância da doxorrubicina no tratamento oncológico. Foram analisadas as possíveis deficiências dos testes requeridos pelas agências reguladoras e quando possível foi sugerido procedimentos para sua melhoria. Ainda nesse sentido, foi destacada a importância do compartilhamento de experiência sobre a regulamentação da nanomedicina entre os países e, mais especificamente, seu potencial para impulsionar o desenvolvimento dessa área no Brasil. Pode-se concluir que os testes toxicológicos preconizados atualmente pelas agências reguladoras dos Estados Unidos da América, União Europeia e no Brasil, apesar de estarem alinhados, não são específicos para a avaliação de nanomedicamentos. Em base às informações disponíveis, não se pode garantir que os dados gerados pela bateria de testes solicitada sejam confiáveis para o estabelecimento de uma relação risco/benefício robusta para os nanomedicamentos. Além disso, foram demonstradas muitas das limitações desses testes e algumas sugestões de melhorias para a condução dos mesmos. Ainda nesse sentido, foi ressaltada a importância da caracterização bio-físico-química de cada nanomedicamento submetido às análises. Com relação à bateria de testes toxicológicos solicitada para a avaliação do DOXIL®, pode-se concluir que seu perfil de segurança não pode ser adequadamente estabelecido pelos testes realizados. Entretanto, os dados de pós-comercialização demonstraram que seu perfil de toxicidade está bem estabelecido e que manteve alinhamento com os resultados obtidos durante o seu desenvolvimento. Não se pode, entretanto, extrapolar este mesmo comportamento para outros casos, os quais deverão seguir normativas atualizadas. À luz dessas diferenças e limitações, este estudo traz à discussão os esforços para entender melhor a aplicabilidade dos requisitos atuais de avaliação toxicológica para aprovação de nanomedicamentos e visa contribuir com a ANVISA para a implementação de um programa de avaliação toxicológica robusto para garantir o desenvolvimento seguro da nanomedicina. / Nanotechnology is a transdisciplinary technology which is under developement and is being applied in various fields, among those it is worth highlighted in health, especially with regard to the therapy and diagnosis. Oncologic treatments are very long and expensive, the need for imaging studies is frequent, treatment doses are very high and toxicity is often the limiting therapy factor for patients. The advances in nanotechnology bring a promise expectation to overcome these deficiencies and even mitigate it, taking into consideration some particular characteristics of these materials. However, there is still no clear relationship between these characteristics and their toxicological effects and more studies on this field need to be done in order to validate this as an efficient therapy alternative for those patients. Therefore, it is necessary to understand if the current regulatory requirements in terms of toxicological assessment for registration of a drug based on nanotechnology are able to identify the possible risks arising from this new technology. This study aimed to compare the regulatory approach of the EMA, FDA and ANVISA regarding the evaluation of nanodrugs compared with conventional medicines. For this, the toxicological profile of DOXIL® compared to conventional doxorubicin were reviewed. This product was chosen to be analyzed by being the first liposome approved by FDA in 1995, and the importance of doxorubicin in cancer treatment. Possible shortcomings of the tests required by regulatory agencies and possible suggested procedures for improvement were analyzed. Also in this sense, was highlighted the importance of sharing experience on nanomedicine regulation across countries, and more specifically, its potential to boost the development of this area in Brazil. It was concluded that toxicological tests currently recommended by regulatory agencies in the United States, European Union and Brazil, although they are aligned, are not specific to the assessment of nanodrugs. Based on the available information, it cannot guarantee the reliability of the data generated through the battery of tests required for establishing a robust risk / benefit ratio for nanodrugs. Moreover, were demonstrated many of the limitations of these tests and some suggestions for improvement on the conduction of such investigations. Also in this sense, was highlighted the importance of biophysicochemical characterization of each nanomedicine subjected to analysis. It could be concluded that the DOXIL® safety profile were not adequately represented by the toxicological tests performed for regulatory approval. However, the post-marketing data sustain that its toxicity profile is well established and maintained in alignment with the results obtained during its development. Notwithstanding, it is not possible to extrapolate the same behavior for other cases, which should follow new standards. In light of these discrepancies and limitations, this study brings to discussion the efforts to understand better the applicability of current toxicological assessment requirements for nanomedicines approval and aims to contribute with ANVISA to implement a robust toxicological assessment program to guarantee the safe development of nanomedice.

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro de Ciências da Saúde, Programa de Pós-Graduação em Enfermagem, Florianópolis, 2016. / Made available in DSpace on 2017-06-27T04:04:51Z (GMT). No. of bitstreams: 1 345794.pdf: 1161356 bytes, checksum: a3e407c3f20f7c42e699be6a8fe1d6e6 (MD5) Previous issue date: 2016 / No Brasil, as políticas públicas de saúde reforçam a importância do acompanhante de livre escolha da mulher durante o processo parturitivo. Nos últimos anos, a inserção do companheiro/pai do bebê tem ganhado destaque como uma estratégia para fortalecer e estimular o vínculo familiar e afetivo precocemente. Este estudo objetivou pesquisa foi compreender a experiência da mulher e seu companheiro que permaneceram juntos durante todo o trabalho de parto, mas que não puderam compartilhar o momento do nascimento, devido à necessidade de cesárea. Trata-se de uma pesquisa qualitativa, exploratório-descritiva. A coleta de dados ocorreu de janeiro a julho de 2016, em uma Maternidade Pública da Região Serrana de Santa Catarina, através de entrevistas semiestruturadas, gravadas, a partir de um roteiro temático. Foram entrevistadas as puérperas e seus companheiros que compartilharam o trabalho de parto e no momento do nascimento por cesárea foram separados. A análise dos dados foi através da Análise de Conteúdo de Bardin, com o auxílio do software Atlas.ti 7.0. Participaram 26 sujeitos (13 acompanhantes e 13 puérperas), a idade das mulheres variou de 18 a 36 anos, os companheiros tinham entre 19 e 38 anos. Os resultados são apresentados sob a forma de dois manuscritos, o primeiro intitulado: Juntos no trabalho de parto e separados na cesárea: experiência da mulher e seu companheiro, apresenta três categorias - O apoio do acompanhante durante o trabalho de parto; - Expectativa da mulher e seu companheiro em compartilhar o nascimento e O momento da separação. A experiência de compartilhar o trabalho de parto foi positiva, as mulheres sentiram-se seguras e amparadas pelos seus companheiros que se consideraram importantes nesse processo. Nesse manuscrito foi possível constatar que a expectativa de compartilhar o nascimento não concretizada, gerou sentimentos negativos e frustração na mulher e em seu companheiro. No segundo manuscrito: Separação da mulher e seu acompanhante no nascimento por cesárea: uma violação de direito, emergiram três categorias: - Experiência da mulher em não ter acompanhante na sala cirúrgica; - Experiência do acompanhante em aguardar o nascimento sozinho; e o Poder dos profissionais de saúde sobre a cena do nascimento. Sentimentos negativos, como insegurança e medo estiveram presentes na sala cirúrgica, pois ao ser separada de seu acompanhante a mulher sentiu-se desamparada em um ambiente desconhecido, seus companheiros ficaram decepcionados em não poder compartilhar o nascimento de seu filho, como haviam idealizado ao longo da gestação. Os resultados dessa pesquisa mostram que compartilhar o nascimento do filho é importante para a mulher e seu companheiro/pai do bebê. O principal fator que contribui para separação no nascimento é a atitude dos profissionais envolvidos na assistência que ainda impedem a presença do acompanhante na sala cirúrgica, e o desconhecimento da Lei do acompanhante por parte dos participantes. Os profissionais de precisam refletir sobre o impacto das suas atitudes sobre a experiência vivida pela mulher e seu companheiro/pai do bebê, mudar de conduta e propiciar condições para que um direito amparado por Lei seja respeitado.<br> / Abstract : In Brazil, public health policies have reinforced the importance of an adult companion with the woman in labor. During the last years, the inclusion of the baby's father/ husband/partner has been pointed out as a strategy to empower and stimulate precocious family connection and emotional bond. This research aimed to understand the experience of women and their partners who stayed together during laboring but they could not experience the childbirth due to caesarian section. It is a qualitative, exploratory-descriptive research. Data was collected from January to July, 2016, in a public maternity hospital located in the Mountain Region of Santa Catarina, through semi-structured and recorded interviews from a thematic script. It was interviewed new mothers and their partners who were together during laboring but at caesarian birth have been separated. Data analysis was performed through Content Analysis by Bardin using Atlas.ti 7.0 software. A total of 26 subjects (13 new mothers and 13 partners) were interviewed; women's age rated from 18 to 36 years-old, and partners' age rated from 19 to 38. Results are showed in two documents; the first one named: Together in laboring and separated at caesarian section: the experience of the woman and her partner, shows three categories - The partner's support during laboring; - Expectations of woman and her partner in sharing childbirth; and - The time of the couple's separation. The experience of the labor sharing was positive, when women felt secure and supported by their partners whom considered themselves really important in that process. Expectations on sharing the childbirth were not fulfilled when woman was submitted to caesarian section, so resulting in negative feelings and frustration for both parents. The second document named:Separation of the woman and her companion at birth by cesarean: a violation of law, gave rise to three categories: - Experience of the woman without an adult companion in operating room; - Experience of the partner in waiting the childbirth alone; and - The power of healthcare professionals on childbirth. There were negative feelings as insecurity and fear in operating room because women felt helpless in an unknown environment when they had been separated from their partners, who were disappointed they could not share their childbirth as they dreamed during pregnancy. Results showed that sharing childbirth is essential for woman and her partner/ baby's father. The main contributing factor for separation in childbirth is the attitude of the healthcare professionals who sometimes prevent the presence of the woman's partner in operating room without considering the right for an adult companion. Healthcare professionals haveto think about the impact their attitudes on the woman's and her partner's experience in order to respect the Law.

O crescimento da complexidade e do tamanho dos sistemas computacionais atuais suscitou um aumento na dificuldade de extração e especificação de modelos formais desses sistemas, tornando essa atividade cada vez mais dispendiosa, tanto em tempo quanto em custo. Modelos são utilizados em diversas técnicas da Engenharia de Software, com o intuito de auxiliar em processos que compreendem desde o desenvolvimento de novos softwares, até reconstrução de um sistema a partir de software legado, passando pela realização de manutenção de um software em operação. Portanto, é necessário que essas abstrações sejam confiáveis e representem fielmente o software real. Nesse sentido, a adoção de métodos formais para a construção e análise de modelos computacionais é crescente e motivada, principalmente, pela confiabilidade que os formalismos matemáticos agregam aos modelos. No entanto, a utilização de métodos formais geralmente demanda um alto investimento de recursos humanos e, consequentemente, financeiros, uma vez que a utilização de tais formalismos é condicionada ao estudo profundo de sua fundamentação matemática. Considerando-se a extensa aplicabilidade de modelos em diversas subáreas da Ciência da Computação e as vantagens advindas da utilização de métodos formais para especificar sistemas, é interessante identificar métodos e ferramentas existentes para automatizar os processos de extração e análises de modelos, em conjunto com a adoção de formalismos que possam ser utilizados por profissionais da computação que atuam na indústria de software. Dessa forma, é estimulada nesse trabalho a utilização do formalismo de Gramática de Grafos, um método formal que diferencia-se dos demais por ser intuitivo e possuir uma representação visual gráfica, o que facilita a sua compreensão e não exige um conhecimento avançado sobre o formalismo. Primeiramente, é proposta uma abordagem para a extração de modelos em Gramática de Grafos a partir de código-fonte, extraindo informações de execuções de código Java anotado. Em seguida, é apresentada uma metodologia existente para extração e análise de Gramática de Grafos a partir de Casos de Uso, juntamente com um estudo empírico realizado a fim de validar a metodologia. Por fim, são propostas possíveis verificações adicionais, a fim de extender as análises dessa metodologia. Com isso, busca-se a obtenção de modelos, descritos através do formalismo de grafos, a partir de artefatos criados nos dois pólos do processo de desenvolvimento de software, antes e depois da implementação, no sentido de viabilizar futuras comparações, no contexto de verificação de software. / The growing size and complexity of current computer systems leading to an increase in the difficulty of extraction and specification of formal models of such systems, making it increasingly expensive activity, both in time and in cost. Models are used in various techniques of software engineering in order to assist in processes that range from the development of new software, to rebuild a system from legacy software, passing for performing maintenance of software in operation. Therefore, it is necessary that these abstractions are reliable and faithfully represent the actual software. In this sense, the adoption of formal methods for the construction and analysis of models is growing and motivated mainly by the reliability that the mathematical formalism add to models. However, the use of formal methods generally demands a high investment in human resources and hence financial, since the use of such formalism is conditioned to the deep study of its mathematical foundation. Considering the extensive applicability of models in various subfields of computer science and the benefits arising from the use of formal methods for specifying systems, it is interesting to identify existing methods and tools to automate the process of extracting models, in addition to the adoption of formalism that can be used by computer professionals working in the software industry. Thus, we encourage the use of the Graph Grammar formalism, a formal method that differs from others because it is intuitive and has a graphical visual representation, making it easy to understand and does not require an advanced knowledge of the formalism. First, we propose an approach for extracting models from source code in Graph Grammar, getting information of executions of annotated Java code. Then an existing methodology for extraction and analysis of Graph Grammar from Use Cases is presented, along with an empirical study to validate the methodology. Finally, we propose possible additional checks in order to extend the analysis of this methodology. Thus, this work aims to extract models, described by the formalism of graphs, from artifacts created in the two poles of the software development process, before and after implementation, in order to allow future comparisons, in the context of software verification.

A integração estruturada e consistente de diversas especificações (ou visões) de um sistema é hoje uma questão essencial na moderna abordagem para especificação e desenvolvimento de software. Neste contexto, precisamos de uma teoria que fale sobre formalismos de especificação e que ao mesmo tempo nos ofereça conceitos e construções para estabelecer-mos relações entre eles. Com este trabalho temos o objetivo de discutir noções rigorosas para idéia de lógica, técnicas fundamentais para relacioná-Ias e mostrar a utilização destes concei¬tos para abordar a questão da interoperabilidade formal, especialmente de provas. Como formalização para idéia de lógica utilizaremos as Instituições de Goguen & Burstall e a extensão de Meseguer para General Logics. Como técnica para rela¬cionar lógicas trabalharemos com os mapeamentos Plain e Simples de Meseguer. Atenção especial é dada à discussão das propriedades destes mapeamentos com vis¬ta à reutilização de componentes lógicos, especialmente da relação de consequência entre fórmulas. Contribuições desta dissertação incluem um tratamento acessível para os con¬ceitos fundamentais necessários para estudar lógicas e sua integração, uma expo¬sição uniforme e detalhada de uma família de sistemas lógicos e uma apresentação categórica desta integração via mapeamentos. / The integration in a sound and structured way of several specifications (or views) of a system is a key research area in (modern) software specification and development. In this context, we need a theory to speak not only about specification logics, but also one that can offer us concepts and constructions to establish relations between these formalisms. In this work we have the purpose of discussing rigorous notions for the idea of logic, presenting fundamental techniques to relate them, and introducing important constructions to approach the problem of formal interoperability, most notably of proofs. As a formalization of the informal idea of a logical system, we use Goguen & Burstall's concept of Institutions and Meseguer's further extension to General Logics. Meseguer's Plain and Simple Maps of Institutions are the tools we use to relate and map logics. Besides, special attention is given for the discussion of the essential properties of these maps concerning the borrowing of logical components, specially of consequence relations. Contributions of this thesis include a smooth presentation of fundamental techniques to study and relate logics, an uniform and detailed exposition of a num¬ber of logical systems, and a categorical formalization of relations between these formalisms by way of maps between institutions.

Submitted by Viviane Lima da Cunha (viviane@biblioteca.ufpb.br) on 2015-12-07T12:53:08Z No. of bitstreams: 1 arquivototal.pdf: 1399886 bytes, checksum: 8212641c2f113601c40bfdf113b9b2ef (MD5) / Made available in DSpace on 2015-12-07T12:53:08Z (GMT). No. of bitstreams: 1 arquivototal.pdf: 1399886 bytes, checksum: 8212641c2f113601c40bfdf113b9b2ef (MD5) Previous issue date: 2015-08-21 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - CAPES / This paper is a research, interventionist and applied, involving formal oral genres, which culminated in an opinion debate with students from 9th grade of a public school in Joao Pessoa (PB) on "Marijuana: Keep prohibition or decriminalize?". We assume that orality, particularly in formal situations, it is forgotten by the school, which compromises the integral formation of Portuguese-speaking students and therefore should be encouraged in the classroom. The main purpose of the procedure was equip students for responsible and critic production of oral texts, especially in the formal mode, teaching them to use the language in an appropriate manner, in all contexts. As an intervention parameter, we rely (with adjustments) in the model of didactic sequence by Dolz, Noverraz and Schneuwly (2004), taking into account strategies that enable students to understand and produce texts appropriate to the genre in question, considering its style, subject content and compositional structure (Bakhtin, 1997) and also had developed his argumentative skills. As theoretical support, we resort to Antunes (2003), Reyzábal (1999), Koch (2011) and Marcuschi (1997, 2007, 2010), that supported us in the understanding of oral language, reading, writing, oral genres and debate. Besides Preti (2004) and Ramos (1997), which contributed to the study of linguistic register and formal oral genres and Ribeiro (2009); Fiorin (2015) and Piglet (2011), dealing with concepts of argument, counter-argument and argumentative resources. Our analysis was based on comparing the first production (the theme homophobia) and the latter considered the work developed during the modules. It was possible to detect advances as the characterization by students of the genre of opinion debate, from the articulation of its three constituent elements and the formulation of points of linguistic view, semantics and articulated arguably, with the use of resources as the exemplification, the exposure facts and transitivity. At the end, we present a suggested teaching sequence on the gender opinion debate, based on our practice of the classroom. / O presente trabalho trata de uma investigação, de caráter intervencionista e aplicada, envolvendo gêneros orais formais, que culminou na realização de um debate de opinião com alunos do 9º ano de uma escola estadual de João Pessoa (PB) sobre o tema “Maconha: Manter Proibição ou Descriminalizar?”. Partimos do pressuposto de que a oralidade, principalmente em situações formais, é esquecida pela escola, o que compromete a formação integral de estudantes de Língua Portuguesa e, por isso, deve ser incentivada em sala de aula. O principal objetivo do procedimento foi instrumentalizar os estudantes para a produção competente e crítica de textos orais, especialmente na modalidade formal, ensinando-os a usar a língua, de forma adequada, em todos os contextos. Como parâmetro de intervenção, nos baseamos (com adaptações) no modelo de sequência didática de Dolz, Noverraz e Schneuwly (2004), levando em conta estratégias que permitissem aos estudantes compreender e produzir textos adequados ao gênero em questão, considerando seu estilo, conteúdo temático e estrutura composicional (BAKHTIN, 1997) e ainda tivessem desenvolvidas suas capacidades argumentativas. Como aporte teórico, recorremos a Antunes (2003), Reyzábal (1999), Koch (2011) e Marcuschi (1997, 2007, 2010), que nos subsidiaram no entendimento sobre oralidade, leitura, escrita, gêneros orais e debate. Além de Preti (2004) e Ramos (1997), que contribuíram no estudo do registro linguístico e gêneros orais formais e Ribeiro (2009); Fiorin (2015) e Leitão (2011), que tratam dos conceitos de argumentação, contra-argumentação e recursos argumentativos. Nossa análise tomou por base a comparação entre a primeira produção (cujo tema foi homofobia) e a última, considerado o trabalho desenvolvido durante os módulos. Foi possível detectar avanços como a caracterização, pelos alunos, do gênero debate de opinião, a partir da articulação de seus três elementos constituintes e a formulação de pontos de vista linguística, semântica e argumentativamente articulados, com o uso de recursos como a exemplificação, a exposição de fatos e a transitividade. Ao final, apresentamos uma sugestão de sequência didática sobre o gênero debate de opinião, baseada em nossa prática de sala de aula.

Submitted by RENAN LUCAS DUTRA URBAN null (renanurban@hotmail.com) on 2018-02-21T14:54:14Z No. of bitstreams: 1 Renan Lucas Dutra Urban.pdf: 1172351 bytes, checksum: eabb61466e41dd2220c06c30c872f009 (MD5) / Submitted by RENAN LUCAS DUTRA URBAN null (renanurban@hotmail.com) on 2018-02-22T19:46:16Z No. of bitstreams: 1 Renan Lucas Dutra Urban.pdf: 1172351 bytes, checksum: eabb61466e41dd2220c06c30c872f009 (MD5) / Approved for entry into archive by Andreia Beatriz Pereira null (andreia.beatriz@franca.unesp.br) on 2018-02-26T18:12:46Z (GMT) No. of bitstreams: 1 Urban_RLD_me.fran.pdf: 1172351 bytes, checksum: eabb61466e41dd2220c06c30c872f009 (MD5) / Made available in DSpace on 2018-02-26T18:12:46Z (GMT). No. of bitstreams: 1 Urban_RLD_me.fran.pdf: 1172351 bytes, checksum: eabb61466e41dd2220c06c30c872f009 (MD5) Previous issue date: 2017-12-18 / O objeto do trabalho é a derrotabilidade das regras jurídicas. O objetivo geral é analisar a possibilidade de que uma regra seja derrotada, isto é, seja superada por um princípio que com ela colide. É possível que uma regra seja derrotada e continue existindo como uma regra? Uma colisão entre uma regra e um princípio pode ser solucionada por meio da aplicação de uma cláusula de exceção, decorrente desse princípio? Para responder a essas questões, foram concebidos quatro objetivos específicos, cada um deles correspondente a um capítulo. O primeiro é apresentar o marco teórico do trabalho: a distinção estrutural entre regras e princípios, proposta por Robert Alexy. O segundo é examinar a forma pela qual devem ser solucionados, tipicamente, os conflitos que ocorrem entre, de um lado, as regras, definidas como mandamentos definitivos, e, de outro, os princípios, definidos como mandamentos de otimização. O terceiro é delimitar o conceito de derrotabilidade das generalizações e, especificamente, de derrotabilidade das regras jurídicas. E o quarto é discutir sob quais condições uma colisão entre uma regra e um princípio pode ser solucionada por meio da aplicação deste em detrimento da aplicação daquela. A principal tese defendida consiste na seguinte: é possível que uma regra, desproporcional num caso concreto, seja derrotada e, mesmo assim, tenha seu caráter definitivo preservado. Quando os órgãos julgadores levam em consideração os fatores institucionais e procedimentais relativos a certos princípios formais – como, por exemplo, os da competência decisória do legislador democraticamente legitimado, da segurança jurídica e da eficiência decisória –, as ocasiões de derrota das regras não implicam a perda do caráter definitivo dessas normas, ou a aquisição, por elas, de um caráter prima facie. Uma regra, quando subótima, sobreinclusiva ou derrotável, continua sendo uma regra quando oferece alguma resistência à sua superação por um princípio que com ela colide; e, desde que essa resistência seja levada a sério pelos tomadores de decisão, uma regra, quando derrotada, continua sendo uma regra, a despeito da introdução, em seu suporte fático, de uma exceção, derivada de um princípio colidente. / The topic of this dissertation is the defeasibility of legal rules. The general objective is to analyze the possibility that a rule is defeated or overcome by a colliding principle. Can a rule still be a rule when it is defeated? Can a collision between a rule and a principle be solved by applying an exception clause, derived from this principle? In order to answer these questions, four specific objectives were designed, each corresponding to a chapter. The first is to introduce the theoretical framework of this research: the structural distinction between rules and principles, proposed by Robert Alexy. The second is to examine how conflicts between rules, defined as definitive requirements, and principles, defined as optimization requirements, should be typically resolved. The third is to delimit the concept of defeasibility of generalizations and, specifically, of defeasibility of legal rules. The fourth is to discuss under what conditions a collision between a rule and a principle can be solved by applying the principle. The main thesis is as follows: it is possible that a rule, disproportional in a concrete case, is defeated and, nevertheless, has its definitive character preserved. Rules do not lose their definitive character or assume a prima facie character if, in the cases in which they are defeated, institutional factors relating to certain formal principles – such as those of the democratically legitimated legislature, legal certainty, and efficiency – are taken into account. A rule, when suboptimal, over-inclusive or defeasible, is still a rule when it offers some resistance to its overcoming by a colliding principle; and insofar as this resistance is taken seriously by decision-makers, a rule, when defeated, is still a rule, despite the introduction, in its factual predicate, of an exception derived from a colliding principle.