Submitted by Irene Nascimento (irene.kessia@ufpe.br) on 2016-11-08T19:13:18Z No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) Dissertação_Final.pdf: 15901621 bytes, checksum: e3bd1c1be70941932d970f61be02e4c1 (MD5) / Made available in DSpace on 2016-11-08T19:13:18Z (GMT). No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) Dissertação_Final.pdf: 15901621 bytes, checksum: e3bd1c1be70941932d970f61be02e4c1 (MD5) Previous issue date: 2015-02-25 / O processo de identificação de um determinado indivíduo é realizado milhões de vezes, todos os dias, por organizações dos mais diversos setores. Perguntas como "Quem é esse indivíduo?" ou "É essa pessoa quem ela diz ser?" são realizadas frequentemente por organizações financeiras, sistemas de saúde, sistemas de comércio eletrônico, sistemas de telecomunicações e por instituições governamentais. Identificação biométrica diz respeito ao processo de realizar essa identificação a partir de características físicas ou comportamentais. Tais características são comumente referenciadas como características biométricas e alguns exemplos delas são: face, impressão digital, íris, assinatura e voz. Reconhecimento de locutores é uma modalidade biométrica que se propõe a realizar o processo de identificação pessoal a partir das informações presentes unicamente na voz do indivíduo. Este trabalho foca no desenvolvimento de sistemas de verificação de locutores independente de texto. O principal desafio no desenvolvimento desses sistemas provém das chamadas incompatibilidades que podem ocorrer na aquisição dos sinais de voz. As técnicas propostas para suavizá-las são chamadas de técnicas de compensação e três são os domínios onde elas podem operar: no processo de extração de características do sinal, na construção dos modelos dos locutores e no cálculo do score final do sistema. Além de apresentar uma vasta revisão da literatura do desenvolvimento de sistemas de verificação de locutores independentes de texto, esse trabalho também apresenta as principais técnicas de compensação de características, modelos e scores. Na fase de experimentação, uma análise comparativa das principais técnicas propostas na literatura é apresentada. Além disso, duas técnicas de compensação são propostas, uma do domínio de modelagem e outra do domínio dos scores. A técnica de compensação de score proposta é baseada na Distribuição Normal Acumulada e apresentou, em alguns contextos, resultados superiores aos apresentados pelas principais técnicas da literatura. Já a técnica de compensação de modelo é baseada em uma técnica da literatura que combina dois conceitos: treinamento multi-condicional e Teoria dos Dados Ausentes (Missing Data Theory). A formulação apresentada pelos autores é baseada nos chamados Modelos de União a Posteriori (Posterior Union Models), mas não é completamente adequada para verificação de locutores independente de texto. Este trabalho apresenta uma formulação apropriada para esse contexto que combina os dois conceitos utilizados pelos autores com um tipo de modelagem utilizando UBMs (Universal Background Models). A técnica proposta apresentou ganhos de desempenhos quando comparada à técnica-padrão GMM-UBM, baseada em Modelos de Misturas Gaussianas (GMMs). / The personal identification of individuals is a task executed millions of times every day by organizations from diverse fields. Questions such as "Who is this individual?" or "Is this person who he or she claims to be?" are constantly made by organizations in financial services, health care, e-commerce, telecommunication systems and governments. Biometric identification is the process of identifying people using their physiological or behavioral characteristics. These characteristics are generally known as biometrics and examples of these include face, fingerprint, iris, handwriting and speech. Speaker recognition is a biometric modality which makes the personal identification by using speaker-specific information from the speech. This work focuses on the development of text-independent speaker verification systems. In these systems, speech from an individual is used to verify the claimed identity of that individual. Furthermore, the verification must occur independently of the pronounced word or phrase. The main challenge in the development of speaker recognition systems comes from the mismatches which may occur in the acquisition of the speech signals. The techniques proposed to mitigate the mismatch effects are referred as compensation methods. They may operate in three domains: in the feature extraction process, in the estimation of the speaker models and in the computation of the decision score. Besides presenting a wide description of the main techniques used in the development of text-independent speaker verification systems, this work presents the description of the main feature-, model- and score-based compensation methods. In the experiments, this work shows comprehensive comparisons between the conventional techniques and the alternatively compensations methods. Furthermore, two compensation methods are proposed: one operates in the model domain and the other in the score-domain. The scoredomain proposed compensation method is based on the Normal cumulative distribution function and, in some contexts, outperformed the performance of the main score-domain compensation techniques. On the other hand, the model-domain compensation technique proposed in this work is based on a method presented in the literature which combines two concepts: the multi-condition training and the Missing Data Theory. The formulation proposed by the authors is based on the Posterior Union models and is not completely appropriate for the text-independent speaker verification task. This work proposes a more appropriate formulation for this context which combines the concepts used by the authors with a type of modeling using Universal Background Models (UBMs). The proposed method outperformed the usual GMM-UBM modeling technique, based on Gaussian Mixture Models (GMMs).

Submitted by Miriam Lucas (miriam.lucas@unioeste.br) on 2018-02-22T14:23:15Z No. of bitstreams: 2 Felipe_Crestani_dos_Santos_2017.pdf: 5495370 bytes, checksum: 82f81445874bba45497cda5c8d784d2f (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Made available in DSpace on 2018-02-22T14:23:15Z (GMT). No. of bitstreams: 2 Felipe_Crestani_dos_Santos_2017.pdf: 5495370 bytes, checksum: 82f81445874bba45497cda5c8d784d2f (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Previous issue date: 2017-11-17 / The main line of research of this work is the study of approaches for supporting the development and analysis of the Power System Protection. In general, this process is carried out through of a large number of simulations involving various operating scenarios. The main limitation of this technique is the impossibility of coverage of all behavior of the system under analysis. In this context, this work proposes the use of Model Checking as a tool to support the procedure of development of power system protection schemes, principally in the sense of proving the security requirements and temporal deterministic expected behavior. Model Checking is a verification technique that explores exhaustively and automatically all possible system states, checking if this model meets a given specification. This work focuses on this two pillars of the Model Checking: to choose an appropriate modeling formalism for representation of the power system protection and how to describe the specification in temporal-logic for the verification process. With regard to the modeling formalism, the power system protection will be represented by the Hybrid Automata theory, while the verification tool adopted will be Statistical Model Checking, by the UPPAAL STRATEGO toolkit. It is underlined that this work is limited to the modeling of individual components of the power system protection, such that 18 models of the devices and protocols like communication bus (LAN), time synchronization protocol (PTP) and IEC 61850 communication protocols (SV and GOOSE) and Logical Nodes of power system protection, and 13 auxiliaries models, which emules the stochastic behavior to subsidise the verification process. The methodology of modelling adopted guarantees the effective representation of the components behaviour of power system protection. For this, the results of Model Checking process were compared with behavioral requirements defined by standards, conformance testings and paper related to the area. With regard to the contributions of this work, were identified three researches areas that could use the models developed in this work: i) implementation of power system protection schemes; ii) achievement of conformance testing; and iii) indication of the parameterization error of the power protection system scheme. / A linha de pesquisa abordada neste trabalho aponta para o estudo e desenvolvimento de ferramentas que subsidiem a proposição e validação de Sistemas de Proteção de Sistemas de Energia Elétrica. Em geral, este processo é realizado mediante simulações computacionais envolvendo diversos cenários de operação e distúrbios, tendo como principal limitação a impossibilidade de representar todos os caminhos de evolução do sistema em análise. Nesse contexto, propõe-se o emprego da técnica de Modelagem e Verificação Formal como ferramenta de suporte ao projeto, análise e implementação de estratégias de proteção, principalmente no sentido de comprovar se a estratégia atende os requisitos de segurança e comportamento determinístico temporal esperado. Em síntese, o método consiste na verificação de propriedades descritas em lógicas temporais, sob uma abstração apropriada (formalismo) do comportamento do sistema. Esta dissertação possui enfoque nestes dois requisitos: modelagem do sistema de proteção através de um formalismo adequado e tradução dos requisitos do comportamento desejado em propriedades descritas em lógica temporal. Com relação ao formalismo de apoio, a modelagem do sistema de proteção é baseada em uma abstração de Autômatos Temporizados Híbridos. Como ferramenta de validação, adota-se a técnica de Verificação Formal Estatística, através do software UPPAAL STRATEGO. Salienta-se que este trabalho se delimita apenas na modelagem e validação individual dos principais equipamentos de um sistema de proteção, sendo 18 modelos de dispositivos e protocolos como barramentos de comunicação (LAN), protocolo de sincronização de tempo PTP, protocolos de comunicação baseados em IEC 61850 e funções de proteção, e 13 modelos auxiliares que implementam um comportamento estocástico para subsidiar o processo de validação do sistema de proteção. O desenvolvimento dos modelos se deu através de uma abordagem sistemática envolvendo processos de simulação e verificação das propriedades sob o modelo em análise. Através desta metodologia, garante-se que os modelos desenvolvidos representam o comportamento esperado de seus respectivos dispositivos. Para isso, os resultados do processo de verificação foram comparados com requisitos comportamentais definidos por normas, testes de conformidade em equipamentos/protocolos e trabalhos acadêmicos vinculados à área. Com relação às contribuições do trabalho, identificou-se três linhas de pesquisa que podem fazer o uso dos modelos desenvolvidos: i) implementação de novas estratégias de proteção; ii) realização de testes de conformidade em equipamentos externos à rede de autômatos; e iii) indicação de erros de parametrização do sistema de proteção.

Submitted by Wagner Junior (wagner.junior@unioeste.br) on 2018-11-30T17:04:04Z No. of bitstreams: 2 Claudia_Beatriz_Bozz_2018.pdf: 4791914 bytes, checksum: 0affba2e984ec7e6beefa83d0c3bdfeb (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Made available in DSpace on 2018-11-30T17:04:04Z (GMT). No. of bitstreams: 2 Claudia_Beatriz_Bozz_2018.pdf: 4791914 bytes, checksum: 0affba2e984ec7e6beefa83d0c3bdfeb (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Previous issue date: 2018-07-26 / Real time systems that have continuous behavior associated with discrete elements are called hybrid systems. Among them, in this master’s research, a hydraulic system has been chosen as an object of study in order to perform the reliability analysis of it through modeling and formal verification. Much as several models for the reliability analysis of complex systems have been proposed in the literature, most of them are not suitable to represent the system when its behavior needs to be expressed by means of continuous variables, like the case of hybrid systems. Generally, simulation and experimental testing are used to analyze systems, and they give only approximate results from a large amount of samples. To eliminate the limitations of these techniques, the formal verification is an effective alternative, since it is characterized by performing a sweep in all possible states of the system automatically, verifying the behavior as a whole. The UPPAAL STRATEGO toolkit for modelling by stochastic hybrid automata and model checking has been used in this work, both classic formal verification and statistical formal verification. A benckmark has been used as object of study. Initially, the system has been modelling and its behavior (physical and controlled) verified through simulation and formal verification (property specification and model checking). The reliability parameters obtained in the statistical analysis of the system failures have been compared with results of literature, presenting a dispersion less than 2.5%, so it can be verify that the methodology used and the models constructed were adequate to analyze the reliability of this system hybrid.In a second step of this work, the probability distribution of failure of the components have been modified, in order to become the system more reliable with real hydraulic systems, and estimate the optimum mean time between maintenance (MTBM) of this system. Thus, it’s possible to conclude that the methodology is adequate to perform the reliability analysis of the hydraulic system, being that model checking is effective to estimate the reliability parameters of the hydraulic system. / Sistemas de tempo real que possuem comportamento contínuo associado com elementos de características discretas são chamados de sistemas híbridos. Dentre estes, nesta pesquisa de mestrado, optou-se pelo emprego de um sistema hidráulico como objeto de estudo a fim de realizar a análise de confiabilidade do mesmo a partir de modelagem e verificação formal. Por mais que diversos modelos para a análise de confiabilidade de sistemas complexos tenham sido propostos na literatura, a maioria não são adequados para representar sistemas em que o comportamento é expresso em variáveis contínuas, como é o caso dos sistemas híbridos. De modo geral, para a análise de sistemas, a simulação e os testes experimentais são comumente utilizados, e geram apenas resultados aproximados a partir de uma grande quantidade de amostras. Para eliminar as limitações destas técnicas, a verificação formal é uma alternativa eficaz, visto que é caracterizada por realizar uma varredura em todos os estados possíveis do sistema de forma automática, verificando o comportamento como um todo do mesmo. Neste trabalho, foi utilizada a ferramenta computacional UPPAAL STRATEGO para a modelagem por autômatos estocásticos híbridos e verificação dos modelos, tanto verificação formal clássica como estatística. Um modelo padrão (benchmark) foi utilizado como objeto de estudo. Inicialmente o sistema foi modelado e seu comportamento (físico e controlado) verificado através da simulação e verificação formal (especificação de propriedades e verificação de modelos). Os parâmetros de confiabilidade obtidos na análise estatística de falha do sistema foram comparados com outros existentes na literatura, apresentado uma dispersão inferior a 2,5%, logo pôde se verificar que a metodologia empregada e os modelos construídos foram adequados para análise de confiabilidade deste sistema hibrido. Em uma segunda etapa do trabalho, foi modificada a distribuição de probabilidade de falha dos componentes, a fim de tornar o sistema mais fidedigno com sistemas hidráulicos reais, e estimar o tempo médio entre manutenções (MTBM – Mean Time Between Maintenance) ideal deste sistema. Portanto, conclui-se que a metodologia empregada foi adequada para realizar a análise de confiabilidade do sistema hidráulico, sendo efetivo levantar os parâmetros de confiabilidade através da verificação de modelos.

Em decorrência de sua atuação expressiva no mercado de financiamento de empreendimentos de habitação e infraestrutura, a Caixa Econômica Federal (Caixa) é um banco de grande relevância para o setor da construção civil brasileira. A Caixa mantém um setor técnico no qual são desempenhadas, dentre demais responsabilidades, as atividades de análise de documentação técnica e verificação da execução orçamentária e financeira das obras. Atualmente, esses procedimentos são realizados essencialmente de forma manual, configurando um processo moroso e suscetível à ocorrência de imprecisões. Nesse sentido, o presente trabalho tem como objetivo analisar a introdução da Modelagem da Informação da Construção, notadamente, no processo de verificação da documentação técnica de obras, realizado pelos profissionais desse banco público. Primeiramente, realizou-se um diagnóstico, por meio de uma survey, no setor técnico da Caixa que apontou aspectos relevantes à gestão de mudanças de origem tecnológica nesse ambiente. Em continuidade ao estudo de caso, investigou-se as motivações, os benefícios almejados e as possíveis barreiras para a implantação dessa inovação no processo de análise técnica desenvolvido pela instituição. Para verificar a adequabilidade e a aceitação das propostas preliminares de ferramentas e diretrizes de modelagem foi conduzido um workshop no qual participaram profissionais voluntários do mercado da construção civil. Com base neste estudo, apresentado neste trabalho na forma de três artigos científicos publicados, verificou-se que a Caixa pode ser considerada um importante vetor de difusão de práticas associadas à Modelagem da Informação da Construção na indústria da construção civil brasileira e que a proposição de novas ferramentas e diretrizes poderia ser efetivamente adequada para incrementar a prática projetual. Além disso, observou-se que a transformação interna necessária para a implementação de mudanças nos processos técnicos da Caixa é viável desde que seja propiciado um ambiente favorável, em que os gestores incentivem, planejem e deem suporte às possíveis mudanças. Finalmente, a contribuição pretendida com esta pesquisa é fomentar outras iniciativas e colaborar para a disseminação da Modelagem da Informação da Construção nos setores de projeto e construção civil brasileiros. / Due to its outstanding performance in housing and infrastructure construction financing market, Caixa Econômica Federal (Caixa) is a bank of great importance in the Brazilian Construction and Design industry. Caixa maintains a technical department that, among other activities, perform technical feasibility analyses, and verify the budgetary and financial development of construction projects. Currently, the project analysis process is manual, time-consuming and error-prone. In this sense, the present study aims to analyse the introduction of Building Information Modelling in the technical feasibility analyses process, carried out by engineers and architects. Firstly, a survey was conducted to perform an intraorganizational assessment of Caixa\'s technical department, in order to identify aspects relevant to change management. Secondly, in this study case, the motivations, the desired benefits and potential barriers to the implementation of this innovation were investigated. In addition, a workshop was conducted with construction and design professionals to verify the suitability and acceptance of the preliminary proposals of tools and modelling guidelines. Based on this study presented in three published scientific papers, Caixa can be considered an important diffusion vector of Building Information Modelling practices in the Brazilian construction and design industry. In addition, the proposition of new tools and modelling guidelines could effectively be appropriate to enhance its design practices. Furthermore, the intraorganizational change required for implementing innovations in the Caixa technical department proved to be feasible if provided with a favourable environment in which managers stimulate, plan and support possible changes. Finally, the intended contribution of this research is to encourage other initiatives and contribute to spreading additional practices related to Building Information Modelling in the Brazilian construction and design industry.

Orientador: Jacques Wainer / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-12T05:34:50Z (GMT). No. of bitstreams: 1 Dantas_MarcioPaixao_M.pdf: 4152956 bytes, checksum: f995417b653e9759340129be4c4d2608 (MD5) Previous issue date: 2008 / Resumo: Um guia de conduta médica é um documento formado por um conjunto de recomendações sistematicamente desenvolvidas para auxiliar nas decisões de praticantes e pacientes sobre cuidados de saúde em circunstâncias específicas. Desde que sejam bem elaborados, comprovadamente melhoram a qualidade média do atendimento médico. Frequentemente médicos não estão acostumados com guias práticos escritos em papel e não os aplicam adequadamente. Implementados em sistemas computacionais podem melhorar significativamente a qualidade do atendimento médico diretamente no local da assistência. Este trabalho está ligado ao projeto ST-Guide, uma iniciativa surgida no Instituto de Computação da Universidade Estadual de Campinas (IC-UNICAMP) para resolver o problema de formalização e implementação de guias clínicos práticos. As contribuições realizadas foram: (a) reestruturação do projeto em outras tecnologias; (b) estabelecimento e implementação de uma arquitetura extensível para suportar modelagem e implementação de guias; (c) realização de alterações conceituais para facilitar o processo de modelagem; (d) criação de novo algoritmo para verificação lógica de incompletude e ambiguidade; e (e) criação de um ambiente gráfico de desenvolvimento de guias associado a um verificador lógico que atua em tempo real, isto é, à medida em que ocorre a modelagem. Experimentos baseados em guias clínicos para assistência pré-natal e hipertensão são apresentados e o texto é concluído com uma discussão do que foi realizado e sugestão de trabalhos futuros. / Abstract: Clinical guidelines are systematically developed statements to assist practitioner and patient decisions about appropriate health care for specific clinical circumstances. Since well elaborated, they provenly improve medical assistance quality. Oftenly clinicians aren't used to paper written guidelines and don't apply them adequately. Implemented in computer systems guidelines can significantly improve medical care quality directly at the point-of-care. This work is related to ST-Guide project, an initiative arisen at the Institute of Computing of State University of Campinas (IC-UNICAMP) to solve the practice guideline formalization and implementation problems. The contributions done were: (a) project restructuring on other technologies; (b) extensible architecture specification and implementation to support guideline modelling and implementation; (c) conceptual changes to ease modelling; (d) new incompletude and ambiguity logical verification algorithm; and (e) guideline graphical development environment coupled with a real time logical verifier. Experiments based on pre-natal assistence and hypertension clinical guidelines are presented and the text is concluded with a discussion of what was done and future work suggestions. / Mestrado / Mestre em Computação

Submitted by Renata Lopes (renatasil82@gmail.com) on 2017-03-21T12:30:57Z No. of bitstreams: 1 elianeraimundadeoliveiratostes.pdf: 2469357 bytes, checksum: cf6f8e5d454803037ab31ac571dbdf24 (MD5) / Approved for entry into archive by Adriana Oliveira (adriana.oliveira@ufjf.edu.br) on 2017-03-21T13:28:13Z (GMT) No. of bitstreams: 1 elianeraimundadeoliveiratostes.pdf: 2469357 bytes, checksum: cf6f8e5d454803037ab31ac571dbdf24 (MD5) / Approved for entry into archive by Adriana Oliveira (adriana.oliveira@ufjf.edu.br) on 2017-03-21T13:28:33Z (GMT) No. of bitstreams: 1 elianeraimundadeoliveiratostes.pdf: 2469357 bytes, checksum: cf6f8e5d454803037ab31ac571dbdf24 (MD5) / Made available in DSpace on 2017-03-21T13:28:33Z (GMT). No. of bitstreams: 1 elianeraimundadeoliveiratostes.pdf: 2469357 bytes, checksum: cf6f8e5d454803037ab31ac571dbdf24 (MD5) Previous issue date: 2016-12-09 / Este estudo tem por objeto de investigação a aplicabilidade do protocolo de cirurgia segura por profissionais que atuam em centro cirúrgico. Objetivo geral Analisar a atuação da equipe interprofissional de cirurgia na aplicabilidade do protocolo de cirurgia segura de um centro cirúrgico. Os objetivos específicos foram: descrever a completude dos profissionais da equipe interprofissional da equipe interprofissional à aplicação do protocolo de cirurgia segura; conhecer as ações dos profissionais quanto ao gerenciamento de evento adverso no centro cirúrgico, tendo por base o protocolo de Cirurgia Segura da Organização Mundial da Saúde, e analisar a importância da aplicação do checklist de cirurgia segura sob a óptica dos profissionais. Para a fundamentação teórica, utilizaram-se estudos sobre gestão de riscos, segurança do paciente, checklist de cirurgia segura e histórico e definição do centro cirúrgico. A metodologia é de natureza descritiva com abordagem qualitativa. O cenário foi um hospital geral público situado em uma cidade da Zona da Mata mineira. A pesquisa foi realizada em dois momentos: o primeiro foi uma busca nos prontuários de pacientes que foram submetidos a procedimentos cirúrgicos no período de outubro de 2013 a dezembro de 2015 para levantamento da adesão do preenchimento do protocolo de cirurgia segura e o segundo foi realizado através de um questionário semiestruturado, no período de março a maio de 2016, com 40 profissionais que exercem suas atividades laborais no centro cirúrgico. Os dados encontrados foram elencados em quatro categorias temáticas: adesão dos profissionais que compõem a equipe de cirurgia à aplicação do protocolo de cirurgia segura foi possível estratificar o número de cirurgias realizadas trimestralmente, onde foram realizados 6.647 procedimentos cirúrgicos no período analisado e 5.912 impressos de protocolos de cirurgia segura foram preenchidos corretamente, o que equivale à média, nesse período analisado, de 90,2% de preenchimento correto do protocolo de cirurgia segura durante cada procedimento cirúrgico, entendimento do profissional sobre o evento adverso no centro cirúrgico percebe-se que havia o conhecimento sobre o termo evento adverso, porque os posicionamentos estavam em comum acordo com os princípios e diretrizes definidos pela organização mundial de saúde, porém em algumas respostas de alguns profissionais da categoria de medicina e técnico de enfermagem, escreveram mais exemplificando o conceito de evento adverso do que propriamente conceituou este termo. Risco, fato indesejável, prejuízo, falhas ou erro, impactos e danos para o paciente foram termos mencionados pelos participantes, mostrando esse conhecimento parcial acerca do conceito de evento adverso, ações tomadas para o gerenciamento de evento adverso no entendimento dos participantes, percebe-se que as ações tomadas em relação ao gerenciamento do evento adverso nesse cenário seriam como barreiras preventivas por meio da aplicação do checklist de cirurgia segura que inclui a diminuição da morbimortalidade de pacientes cirúrgicos. Além disso, dá às equipes cirúrgicas e aos administradores hospitalares orientações sobre a função de cada um e qual é o padrão de uma cirurgia segura, bem como oferece um instrumento de avaliação uniforme do serviço de vigilância. e a percepção dos profissionais quanto à aplicabilidade do checklist de cirurgia segura, onde nesta última categoria foi avaliado cada etapa do protocolo de cirurgia segura quanto ao grau de importância instituído no questionário foi de extremamente importante a sem importância e também nessa categoria foi apresentado algumas dificuldades elencadas pelos participantes, obtiveram-se respostas de: falta de participação da equipe, lista de verificação muito longa, falta de tempo para o preenchimento dos dados a serem checados, falta de treinamento para implementação do checklist. Observou-se que as dificuldades apontadas circulavam entre enfermeiros, médicos e técnicos de enfermagem. Também se verificou que, entre os profissionais citados, as respostas indicavam não terem dificuldades, no entanto houve respondente (técnico de enfermagem) que mencionou o termo “preguiça” no preenchimento relacionado à parte da medicina. Considerou-se que é necessário investir em educação permanente, sobretudo para sanar as dificuldades no preenchimento do checklist. / This study aims to investigate the applicability of the safe surgery protocol by professionals working in the operating theater. General objective To analyze the performance of the interprofessional team of surgery in the applicability of the protocol of safe surgery of a surgical Center. The stated objectives were: describing the a completeness of professionals of the surgical staff to implement the safe surgery protocol; having knowledge of the actions of the professionals regarding the management of adverse events in the operation theater based on the safe surgery protocol of the World Health Organization, and analyzing the importance of the implementation of the surgical safety checklist from the professionals’ perspective. For a theoretical foundation, it has been used studies on risk management, patient safety, surgical safety and record checklist and the definition of operating theater. The methodology has a descriptive nature with a qualitative approach. The scenario was a general public hospital situated in a town in Zona da Mata mineira. The research was conducted in two stages: the first was a search for the medical records of patients who underwent surgical procedures from October 2013 to December 2015 for the analysis of the safe surgery filling-in protocol and the second was performed through a semi structured questionnaire, from March to May 2016, with 40 professionals who exercise their labor activities in the operating theater. The data we have found were listed in four thematic categories: if the professionals who belong to the surgical staff implemented the safe surgery protocol it was possible to stratify the number of surgeries performed quarterly, where 6,647 surgical procedures were performed in the analyzed period and 5,912 printed safe surgical protocols were filled in correctly, which is equivalent to the average of 90.2% correct filling of the Protocol during each surgical procedure, if they understand the adverse event in the OT, it was perceived that there was knowledge about the term adverse event, because the positions were in agreement with the principles and guidelines defined by the world health organization, but in some answers of some professionals of the category of medicine and nursing technician, they wrote more Exemplifying the concept of adverse event of what properly denominated this term. Risk, undesirable fact, injury, failures or error, impacts and damages to the patient were terms mentioned by the participants, showing this partial knowledge about the concept of adverse event, if they take actions to manage adverse event It is perceived that the actions taken in relation to the management of the adverse event in this scenario would be as preventive barriers through the application of the safe surgery checklist that includes the reduction of the morbimortality of surgical patients. In addition, it gives surgical teams and hospital administrators guidance on the role of each and what is the standard of safe surgery, as well as provides a uniform assessment tool for the surveillance service, and if they had the perception of the applicability of the surgical safety checklist Where in the last category was evaluated each step of the protocol of safe surgery as to the degree of importance instituted in the questionnaire was extremely important the unimportant and also in this category was presented some difficulties listed by the participants, were obtained answers of: lack of participation of the Team, very long checklist, lack of time to fill in the data to be checked, lack of training to implement the checklist. It was observed that the mentioned difficulties circulated among nurses, doctors and nursing technicians. It was also verified that, among the professionals cited, the answers indicated that they did not have difficulties, however there was a respondent (nursing technician) who mentioned the term "laziness" in the filling related to the medicine part. It is considered that it is necessary to invest in permanent education, especially to deal with the difficulties when filling the checklist.

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / The hotel industry has grown over the years due to increased tourism in worldwide. In this sector, feeding is a characteristic, because the concept of hosting is inevitably linked to food. But one concern is that not enough provide food to the guests, is necessary give them a food safe from the point of view of sanitary, in accordance with the current legislation. The aim of this study was to verified the procedures for Good Practices in the areas of food and drink (production of meals) in hotels, in Rio Grande do Sul within the context of the FIFA World Cup 2014, as well as check the sample characteristics. From August to October 2010 in a sample of 12 hotels in Porto Alegre, was applied to a form with open and closed questions about the characteristics of the hotels and the respondents. Was realized a hygienic sanitary diagnosis based on the current legislation through visual evaluation and analysis the adopted procedures. It was found that none of the hotels have the presence of a responsible trained technician. There is a lack of knowledge on the part of the responsible about the hygienic sanitary legislation of food, both at federal as state levels, and the hotels do not have implemented good practices. The percentage of general sanitary adequation, of the areas of food and drink in hotels, was classified as level acceptable and insatisfactory. Through the results, it is suggested that establishments seek to achieve improvements, for that the health of the guest and the image of the establishment are not compromised. / A indústria de hotéis vem crescendo ao longo dos anos devido ao aumento do turismo em nível mundial. Dentro deste setor, a alimentação é uma característica, pois o conceito de hospedagem é inevitavelmente ligado a alimentação. Entretanto há uma preocupação de que não basta somente fornecer uma alimentação para os hóspedes, mas é necessário entregar-lhes um alimento seguro do ponto de vista higiênico-sanitário, em conformidade com a legislação vigente. O objetivo do presente trabalho foi verificar os procedimentos de Boas Práticas na área de Alimentos e Bebidas (produção de refeições), em hotéis do Rio Grande do Sul, inseridos no contexto da Copa do Mundo de Futebol FIFA de 2014, bem como verificar as características dos mesmos. De agosto a outubro de 2010, em uma amostra de 12 hotéis de Porto Alegre-RS, foi aplicado um formulário com perguntas abertas e fechadas sobre as características do hotel e do respondente. Realizou-se um diagnóstico higiênico-sanitário baseado na legislação vigente através de avaliação visual e análise dos procedimentos adotados. Constatou-se que nenhum dos hotéis possuía a presença de um responsável técnico capacitado. Há um desconhecimento por parte dos responsáveis acerca da legislação higiênicosanitária de alimentos, tanto na esfera federal quanto estadual, e os hotéis não possuem Boas Práticas implantadas. A percentagem de adequação higiênicosanitária geral, da área de Alimentos e Bebidas dos hotéis, foi classificada como nível aceitável e insatisfatório. Através dos resultados, sugere-se que os estabelecimentos busquem atingir melhorias, para que a saúde do hóspede e a imagem do estabelecimento não sejam comprometidas.

O teste de software engloba diferentes técnicas, métodos e conceitos capazes de garantir a qualidade dos mais variados tipos de sistemas. Dentre tais técnicas, encontra-se o teste baseado em Máquinas de Estados Finitos (MEFs), que visa a garantir a conformidade entre a implementação e a especificação de um software. Com esse propósito, diversos métodos foram propostos para a geração de seqüências de verificação que garantam cobertura total das possíveis falhas existentes em uma implementação. A maioria dos métodos conhecidos são baseados na utilização de seqüências de distinção. Esse recurso, porem, não existe para toda MEF. Alguns métodos buscam a geração de seqüências de verificação baseados em recursos alternativos as seqüências de distinção, contudo, as seqüências geradas são exponencialmente longas. Este trabalho apresenta um método para geração de seqüências de verificação que visa a reduzir o tamanho das seqüências geradas para o domínio de MEFs que não dispõem de seqüência de distinção. Para isso, o método proposto baseia-se na utilização de conjuntos de distinção. Uma avaliação experimental foi realizada afim de mensurar a redução proporcionada pelo método proposto em relação aos principais métodos existentes na literatura. Com esse intuito, foram geradas MEFs aleatórias sob a perspectiva diferentes fatores. Em relação a variação do número de estados, os resultados indicaram reduções acima de 99; 5% em comparação com os métodos existentes, quando analisadas 75% das MEFs geradas / Software testing involves several techniques, methods, and concepts employed to guarantee a high level of quality in different application domains. Among such techniques, Finite State Machine (FSM) based testing aims to guarantee the conformance between the implementation and the specification of a system under test. In this context, several methods were proposed to generate checking sequences that cover all the possible faults existing in an implementation. Most of these methods are based on a special sequence, named distinguishing sequence, which does not exist for every minimal machine. Some methods were proposed to generate checking sequences based on alternative solutions in order to be applied on FSMs that do not have distinguishing sequences. However, these methods generate checking sequences exponentially long. This work proposes a method to generate checking sequences using identification sets. These sets exist for every minimal FSM and also lead to shorter checking sequences. We conducted an experimental study to compare the proposed method with the main existing methods. In the experiments, we used random FSMs that have different configurations of states, inputs, and outputs. Concerning the variation of number of states, the results show reductions higher than 99:5% in comparison with the existing methods for 75% of the experimented machines

Advances in communicat ions have been unarguably essent ial to enablemodern systems and applicat ions as we know them. Ubiquity has turned into reality, allowing specialised embedded systems to eminent ly grow and spread. That is notably the case of unmanned vehicles which have been creat ively explored on applications that were not as efficient as they currently are, neither as innovative as recent ly accomplished. Therefore, towards the efficient operat ion of either unmanned vehicles and systems they integrate, in addition to communicat ion improvements, it is highly desired that we carefully observe relevant , co-related necessit ies that may lead to the full insert ion of unmanned vehicles to our everyday lives. Moreover, by addressing these demands on integrated solut ions, better resultswill likely be produced. This thesis presentsHAMSTER, theHeAlthy, Mobility and Security based data communication archiTEctuRe for unmanned vehicles, which addresses threemain types of communicat ions: machine-to-machine, machine-to-infrast ructure and internal machine communications. Four addit ional elements on co-related requirements are provided alongside with HAMSTER for more accurate approaches regarding security and safety aspects (SPHERE platform), crit icality analysis (NCI index), energy efficiency (NP plat form) and mobility-oriented ad hoc and infrast ructured communicat ions (NIMBLE platform). Furthermore, three specialised versions are provided: unmanned aerial vehicles (Flying HAMSTER), unmanned ground vehicles (Running HAMSTER) and unmanned surface/ underwater vehicles (Swimming HAMSTER). The architecture validat ion is achieved by case studies on each feature addressed, leading to guidelines on the development of vehicles more likely to meet certificat ion requirements, more efficient and secure communicat ions, assert ive approaches regarding crit icality and green approaches on internal communicat ions. Indeed, results prove the efficiency and effectiveness of HAMSTER architecture and its elements, as well as its flexibility in carrying out different experiments focused on various aspects of communication, which helps researchers and developers to achieve safe and secure communicat ions in unmanned vehicles. / Os avanços na área de comunicações foram indiscutívelmente essenciais para a obtenção de sistemas e aplicações modernos como os o atuais. A computação ubíqua se tornou realidade, permitindo que sistemas embarcados especializados ganhassem espaço e cada vez mais autonomia. Esse é notavelmente o caso de veículos não tripulados que têm sido criativamente explorados em aplicações inovadoras e avançadas. Entretanto, para o funcionamento eficiente desses veículos e sistemas não tripulados, além de melhorias de comunicação, é altamente desejável que as necessidades relevantes co-relacionadas a comunica¸cao sejam cuidadosamente observadas, levando a uma facilitação na inserção de veículos não tripulados em espaços públicos. Além disso, ao abordar essas demandas de modo integrado, as chances de produzir melhores resultados é maior. Esta tese apresenta a HAMSTER, uma arquitetura de comunicação de dados baseada em mobilidade e segurança para veículos não tripulados, que aborda três tipos principais de comunicação: máquina-para- máquina, máquina-para-infraestrutura e comunicações internas. Quatro elementos adicionais co-relacionados são fornecidos juntamente com a arquitetura HAMSTER de modo a prover abordagens mais precisas em relação a aspectos de segurança física e da informação (plataforma SPHERE), análise de criticalidade (índice NCI), eficiência energética (plataforma NP) e comunicações ad hoc e infraestruturadas orientadas a mobilidade (plataforma NIMBLE). Além disso, são fornecidas três versões especializadas: para veículos aéreos não tripulados (Flying HAMSTER), veículos terrestres não tripulados (Running HAMSTER) e veículos submarinos e de superfície não tripulados (Swimming HAMSTER). A validação da arquitetura é obtida por meio de estudos de caso sobre cada recurso abordado, levando a diretrizes sobre o desenvolvimento de veículos mais preparados para atender a requisitos de certificação, comunicação mais eficiente e segura, abordagens assertivas sobre criticidade e abordagens verdes nas comunicações internas. Por fim, os resultados comprovaram a eficiência da arquitetura HAMSTER e os elementos com ela providos, bem como a flexibilidade em realizar experimentos focados em vários aspectos de comunicação, auxiliando na obtenção de comunicações seguras em veículos autônomos.

Multi-agent systems (MASs) can be used to model phenomena that can be decomposed into several interacting agents which exist within an environment. In particular, they can be used to model human and animal societies, for the purpose of analysing their properties by computational means. This thesis is concerned with the automated analysis of a particular kind of such social models, namely, those based on behaviourist principles, which contrasts with the more dominant cognitive approaches found in the MAS literature. The hallmark of behaviourist theories is the emphasis on the definition of behaviour in terms of the interaction between agents and their environment. In this manner, not merely re exive actions, but also learning, drives, and emotions can be defined. More specifically, in this thesis we introduce a formal agent architecture (specified with the Z Notation) based on the Behaviour Analysis theory of B. F. Skinner, and provide a suitable formal notion of environment (based on the pi-calculus process algebra) to bring such agents together as an MAS. Simulation is often used to analyse MASs. The techniques involved typically consist in implementing and then simulating a MAS several times to either collect statistics or see what happens through animation. However, simulations can be used in a more verification-oriented manner if one considers that they are actually explorations of large state-spaces. In this thesis we propose a novel verification technique based on this insight, which consists in simulating a MAS in a guided way in order to check whether some hypothesis about it holds or not. To this end, we leverage the prominent position that environments have in the MASs of this thesis: the formal specification of the environment of a MAS serves to compute the possible evolutions of the MAS as a transition system, thereby establishing the state-space to be investigated. In this computation, agents are taken into account by being simulated in order to determine, at each environmental state, what their actions are. Each simulation execution is a sequence of states in this state-space, which is computed on-the-fly, as the simulation progresses. The hypothesis to be investigated, in turn, is given as another transition system, called a simulation purpose, which defines the desirable and undesirable simulations (e.g., \"every time the agent does X, it will do Y later\"). It is then possible to check whether the MAS satisfies the simulation purpose according to a number of precisely defined notions of satisfiability. Algorithmically, this corresponds to building a synchronous product of these two transitions systems (i.e., the MAS\'s and the simulation purpose) on-the-fly and using it to operate a simulator. That is to say, the simulation purpose is used to guide the simulator, so that only the relevant states are actually simulated. By the end of such an algorithm, it delivers either a conclusive or an inconclusive verdict. If conclusive, it becomes known whether the MAS satisfies the simulation purpose with respect to the observations made during simulations. If inconclusive, it is possible to perform some adjustments and try again. In summary, then, in this thesis we provide four novel elements: (i) an agent architecture; (ii) a formal specification of the environment of these agents, so that they can be composed into an MAS; (iii) a structure to describe the property of interest, which we named simulation purpose; and (iv) a technique to formally analyse the resulting MAS with respect to a simulation purpose. These elements are implemented in a tool, called Formally Guided Simulator (FGS). Case studies executable in FGS are provided to illustrate the approach. / Sistemas multi-agentes (SMAs) podem ser usados para modelar fenômenos que podem ser decompostos em diversos agentes que interagem entre si dentro de um ambiente. Em particular, eles podem ser usados para modelar sociedades humanas e animais, com a finalidade de se analisar as suas propriedades computacionalmente. Esta tese trata da análise automatizada de um tipo particular de tais modelos sociais, a saber, aqueles baseados em princípios behavioristas, o que contrasta com as abordagens cognitivas mais dominante na literatura de SMAs. A principal característica das teorias behaviorista é a ênfase na descrição do comportamento em termos da interação entre agentes e seu ambiente. Desta forma, não apenas ações refl exivas, mas também de aprendizado, motivações, e as emoções podem ser definidas. Mais especificamente, nesta tese apresentamos uma arquitetura de agentes formal (especificada através da Notação Z) baseada na teoria da Análise do Comportamento de B. F. Skinner, e fornecemos uma noção adequada e formal de ambiente (com base na álgebra de processos pi-calculus) para colocar tais agentes juntos em um SMA. Simulações são freqüentemente utilizadas para se analisar SMAs. As técnicas envolvidas tipicamente consistem em simular um SMA diversas vezes, seja para coletar estatísticas, seja para observar o que acontece através de animações. Contudo, simulações podem ser usadas de forma a pertmitir a realização de verificações automatizadas do SMA caso sejam entendidas como explorações de grandes espaços-de-estados. Nesta tese propomos uma técnica de verificação baseada nessa observação, que consiste em simular um SMA de uma forma guiada, a fim de se determinar se uma dada hipótese sobre ele é verdadeira ou não. Para tal fim, tiramos proveito da importância que os ambientes têm nesta tese: a especificação formal do ambiente de um SMA serve para calcular as evoluções possíveis do SMA como um sistema de transição, estabelecendo assim o espaço-de-estados a ser investigado. Neste cálculo, os agentes são levados em conta simulando-os, a fim de determinar, em cada estado do ambiente, quais são suas ações. Cada execução da simulação é uma seqüência de estados nesse espaço-de-estados, que é calculado em tempo de execução, conforme a simulação progride. A hipótese a ser investigada, por sua vez, é dada como um outro sistema de transição, chamado propósito de simulação, o qual define as simulações desejáveis e indesejáveis (e.g., \"sempre que o agente fizer X, ele fará Y depois\"). Em seguida, é possível verificar se o SMA satisfaz o propósito de simulação de acordo com uma série de relações de satisfatibilidade precisamente definidas. Algoritmicamente, isso corresponde a construir um produto síncrono desses dois sistemas de transições (i.e., o do SMA e o do propósito de simulação) em tempo de execução e usá-lo para operar um simulador. Ou seja, o propósito de simulação é usado para guiar o simulador, de modo que somente os estados relevantes sejam efetivamente simulados. Ao terminar, um tal algoritmo pode fornecer um veredito conclusivo ou inconclusivo. Se conclusivo, descobre-se se o SMA satisfaz ou não o propósito de simulação com relação às observações feitas durante as simulações. Se inconclusivo, é possível realizar alguns ajustes e tentar novamente. em resumo, portanto, nesta tese propomos quatro novos elementos: (i) uma arquitetura de agente, (ii) uma especificação formal do ambiente desses agentes, de modo que possam ser compostos em um SMA, (iii) uma estrutura para descrever a propriedade de interesse, a qual chamamos de propósito de simulação, e (iv) uma técnica para se analisar formalmente o SMA resultante com relação a um propósito de simulação. Esses elementos estão implementados em uma ferramenta, denominada Simulador Formalmente Guiado (FGS, do inglês Formally Guided Simulator). Estudos de caso executáveis no FGS são fornecidos para ilustrar a abordagem.