Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico, Programa de Pós-Graduação em Ciência da Computação, Florianópolis, 2017. / Made available in DSpace on 2017-06-27T04:21:32Z (GMT). No. of bitstreams: 1 345872.pdf: 1423815 bytes, checksum: d7ab5e6898d999346ceec9e69c88bedd (MD5) Previous issue date: 2017 / Introdução A verificação funcional do projeto de um sistema com multiprocessamento em chip (CMP) vem se tornando cada vez mais desafiadora por causa da crescente complexidade para suportar a abstração de memória compartilhada coerente, a qual provavelmente manterá seu papel crucial para multiprocessamento em chip, mesmo na escala de centenas de processadores. A verificação funcional baseia-se principalmente na geração de programas de teste aleatórios.Trabalhos Correlatos e Gerador Proposto Embora frameworks de verificação funcional que se baseiam na solução de problemas de satisfação de restrições possuam a vantagem de oferecer uma abordagem unificada para gerar estímulos aleatórios capazes de verificar todo o sistema, eles não são projetados para explorar não-determinismo, que é um importante mecanismo para expôr erros de memória compartilhada. Esta dissertação reporta novas técnicas que se baseiam em lições aprendidas de ambos? os frameworks de verificação de propósitos gerais e as abordagens especializadas em verificar o modelo de memória. Elas exploram restrições sobre endereços e cadeias canônicas de dependência para melhorar a geração de testes aleatórios enquanto mantêm o papel crucial do não-determinismo como um mecanismo-chave para a exposição de erros. Geração de Sequências Ao invés de selecionar instruções aleatoriamente, como faz uma técnica convencional, o gerador proposto seleciona instruções de acordo com cadeias de dependências pré-definidas que são comprovadamente significativas para preservar o modelo de memória sob verificação. Esta dissertação explora cadeias canônicas, definidas por Gharachorloo, para evitar a indução de instruções que, sendo desnecessárias para preservar o modelo de memória sob verificação, resultem na geração de testes ineficazes. Assinalamento de Endereços Em vez de selecionar aleatoriamente padrões binários para servir de endereços efetivos de memória, como faz um gerador convencional, o gerador proposto aceita restrições à formação desses endereços de forma a forçar o alinhamento de objetos em memória, evitar falso compartilhamento entre variáveis e especificar o grau de competição de endereços por uma mesma linha de cache. Avaliação Experimental Um novo gerador, construído com as técnicas propostas, foi comparado com um gerador convencional de testes aleatórios. Ambos foram avaliados em arquiteturas de 8, 16, e 32 núcleos, ao sintetizar 1200 programas de testes distintos para verificar 5 projetos derivados, cada um contendo um diferente tipo de erro (6000 casos de uso por arquitetura). Os testes sintetizados exploraram uma ampla variedade de parâmetros de geração (5 tamanhos de programas, 4 quantidades de posições compartilhadas de memória, 4 mixes de instruções, e 15 sementes aleatórias). Os resultados experimentais mostram que, em comparação com um convencional, o novo gerador tende a expor erros para um maior número de configurações dos parâmetros: ele aumentou em 38% o potencial de expor erros de projeto. Pela análise dos resultados da verificação sobre todo o espectro de parâmetros, descobriu-se que os geradores requerem um número bastante distinto de posições de memória para alcançar sua melhor exposição. Os geradores foram comparados quando cada um explorou a quantidade de posições de memória correspondente à sua melhor exposição. Nestas condições, quando destinados a projetos com 32 núcleos através da exploração de todo o espectro de tamanhos de testes, o novo gerador expôs um tipo de erro tão frequentemente quanto a técnica convencional, dois tipos com 11% mais frequência, um tipo duas vezes, e um tipo 4 vezes mais frequentemente. Com os testes mais longos (64000 operações) ambos os geradores foram capazes de expor todos os tipos de erros, mas o novo gerador precisou de 1,5 a 15 vezes menor esforço para expor cada erro, exceto por um (para o qual uma degradação de 19% foi observada). Conclusões e Perspectivas Com base na avaliação realizada, conclui-se que, quando se escolhe um número suficientemente grande de variáveis compartilhadas como parâmetro, o gerador proposto requer programas de teste mais curtos para expor erros de projeto e, portanto, resulta em menor esforço, quando comparado a um gerador convencional.<br> / Abstract : Albeit general functional processor verification frameworks relying on the solution of constraint satisfaction problems have the advantage of offering a unified approach for generating random stimuli to verify the whole system, they are not designed to exploit non-determinism, which is an important mechanism to expose shared-memory errors. This dissertation reports new techniques that build upon the lessons learned from both - the general verification frameworks and the approaches specifically targeting memory-model verification. They exploit address biasing constraints and canonical dependence chains to improve random test generation while keeping the crucial role of non-determinism as a key mechanism to error exposure. A new generator, built with the proposed techniques, was compared to a conventional random test generator. Both were evaluated for 8, 16, and 32-core architectures, when synthesizing 1200 distinct test programs for verifying 5 derivative designs containing each a different type of error (6000 use cases per architecture). The synthesized tests explored a wide variety of generation parameters (5 program sizes, 4 shared-location counts, 4 instruction mixes, and 15 random seeds). The experimental results show that, as compared to a conventional one, the new generator tends to expose errors for a larger number of parameter settings: it increased by 38% the potential for exposing design errors. By analyzing the verification out-comes over the full parameter ranges, we found out that the generators require quite distinct numbers of shared locations to reach best exposure. We compared them when each generator exploited the location count leading to its best exposure. In such conditions, when targeting32-core designs by exploring the whole range of test lengths, the new generator exposed one type of error as often as the conventional technique, two types 11% more often, one type twice as often, and one type4 times as often. With the longest tests (64000 operations) both generators were able to expose all types of errors, but the new generator required from 1.5 to 15 times less effort to expose each error, except for one (for which a degradation of 19% was observed).

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico. Programa de Pós-Graduação em Ciência da Computação. / Made available in DSpace on 2012-10-19T18:05:21Z (GMT). No. of bitstreams: 0Bitstream added on 2014-09-26T01:55:22Z : No. of bitstreams: 1 187706.pdf: 8361705 bytes, checksum: 9be797cb23f6ee3fb73b769882c5279e (MD5) / Neste trabalho foi implementado um método direto que utiliza a transformada wavelet como o principal recurso para a verificação on-line de assinaturas manuscritas. As assinaturas, obtidas na forma de curvas x(t) e y(t) com o auxílio de uma prancheta digitalizadora, passam por uma etapa de pré-processamento e em seguida são submetidas a uma transformada wavelet. A partir destas funções transformadas, são obtidos números que caracterizam de maneira única cada assinatura. Em seguida, com base nestes números, são estabelecidas medidas de dissimilaridade (distância) entre cada assinatura a ser testada e uma assinatura padrão, previamente escolhida de uma amostra de dez assinaturas fornecidas pelo usuário durante um processo de cadastramento. Assume-se que toda nova assinatura deverá produzir distâncias até a padrão que estejam dentro de uma faixa aceitável em torno de médias verificadas no cadastramento. A determinação destas distâncias é efetuada de maneira não-linear, com o auxílio de uma técnica típica de reconhecimento de sons conhecida como "Dynamic Time Warping" (DTW). Esta técnica permite uma compensação em virtude de variações naturais no ritmo de escrita de cada pessoa a cada nova assinatura. Para recuperar a informação relativa à velocidade, perdida pela uniformização imposta pelo pré-processamento, é utilizada ainda uma outra medida de distância, calculada a partir do desvio das funções de warping para as diagonais correspondentes. A fim de justificar a inclusão da transformada wavelet, foi implementado um segundo sistema de verificação, seguindo uma abordagem em que as funções x(t) e y(t) são diretamente confrontadas com a assinatura padrão. Neste caso, as características são as próprias coordenadas dos pixels que descrevem cada assinatura e as medidas de dissimilaridade passam a ser simplesmente as normas das distâncias entre as curvas, cuja correspondência entre pontos também é determinada com o auxílio do DTW. A partir dos testes desenvolvidos, foram obtidas taxas de erro aceitáveis para este tipo de biometria nos dois sistemas implementados. O bom desempenho do caso em que as wavelets não foram incluídas, no entanto, sugere que, em ambos os sistemas, o principal mecanismo de verificação é a comparação não-linear entre parâmetros efetuada pelo DTW.

[pt] A grande quantidade de dados disponíveis na Web permite aos usuários combinarem e rapidamente integrarem dados provenientes de fontes diferentes, pertencentes ao mesmo domínio de aplicação. Entretanto, combinações de dados construídas a partir de fontes de dados independentes e heterogêneas podem gerar inconsistências e, portanto, confundir o usuário que faz uso de tais dados. Esta tese aborda o problema de criação de uma combinação consistente de dados a partir de fontes de dados mutuamente inconsistentes. Especificamente, aborda o problema de testar quando os dados a serem combinados são inconsistentes em relação a um conjunto pré-definido de restrições. As principais contribuições desta tese são: (1) a formalização da noção de combinação consistente de dados, tratando os dados retornados pelas fontes como uma Teoria de Defaults e considerando uma combinação consistente de dados como uma extensão desta teoria; (2) um verificador de modelos para uma família de Lógicas de Descrição, usado para analisar e separar os dados consistentes e inconsistentes, além de testar a consistência e completude das combinações de dados obtidas; (3) um procedimento heurístico para computar tais combinações consistentes de dados. / [en] With the amount of data available on the Web, consumers can mashup and quickly integrate data from different sources belonging to the same application domain. However, data mashups constructed from independent and heterogeneous data sources may contain inconsistencies and, therefore, puzzle the user when observing the data. This thesis addresses the problem of creating a consistent data mashup from mutually inconsistent data sources. Specifically, it deals with the problem of testing, when data to be combined is inconsistent with respect to a predefined set of constraints. The main contributions of this thesis are: (1) the formalization of the notion of consistent data mashups by treating the data returned from the data sources as a default theory and considering a consistent data mashup as an extension of this theory; (2) a model checker for a family of Description Logics, which analyzes and separates consistent from inconsistent data and also tests the consistency and completeness of the obtained data mashups; (3) a heuristic procedure for computing such consistent data mashups.

Made available in DSpace on 2014-06-12T15:54:36Z (GMT). No. of bitstreams: 2 arquivo7173_1.pdf: 2200485 bytes, checksum: d918d7c9e29d6fef51e4898be0e5a5a4 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2005 / Essa tese apresenta contribuições para o problema de verificação de identidade pessoal através de uma arquitetura que combina as biometrias da face, da assinatura e da dinâmica da digitação. As duas primeiras biometrias foram escolhidas por estarem integradas à vida de grande parte da sociedade e os dispositivos utilizados para capturar os padrões são comuns e de baixo custo. A terceira biometria, dinâmica da digitação, além de ser barata, é uma tecnologia transparente ao usuário. A motivação principal dessa tese é analisar estratégias de combinação de padrões para melhorar o desempenho de sistemas de identificação pessoal. Para tanto, foram identificados e investigados os seguintes pontos: (i) Verificação de assinaturas de tamanhos diferentes usando sete grupos de características: pseudo-dinâmicas, estruturais e invariantes (momentos de Hu, Maitra, Flusser, Simon e Central); (ii) Classi- ficação de faces usando Eigenbands Fusion; (iii) Verificação de autenticidade através da análise da dinâmica da digitação utilizando os tempos de pressionamento e de latência; (iv) Modelagem de uma arquitetura para combinar as três biometrias, além da realização de experimentos, visando à avaliação do desempenho; (v) Investigação do limiar de separação entre regiões que definem usuários autênticos e impostores, por classe, através da distribuição t-Student. Os resultados alcançados com o sistema combinado foram comparados com cada uma das modalidades biométricas separadamente, e mostraram que o sistema integrado conseguiu melhores taxas de acerto

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico, Programa de Pòs-graduação em Engenharia de Automação e Sistemas, Florianópolis, 2010 / Made available in DSpace on 2012-10-25T03:15:55Z (GMT). No. of bitstreams: 1 287047.pdf: 2105803 bytes, checksum: a722cc55acdfaf3252bdf60d781f04b3 (MD5) / Para resolver os problemas associados a verificação de sistemas industriais complexos, como os desenvolvidos para CLPs, são necessárias técnicas de modelagem e verificação formal, como forma de provar que o programa está de acordo com as propriedades esperadas. Neste trabalho é proposto um modelo de tradução da linguagem Diagrama Ladder de CLPs para uma linguagem intermediária de verificação FIACRE, que está inserida em uma cadeia de verificação formal do projeto Topcased. Esta abordagem segue o paradigma da engenharia dirigida a modelos e consiste em transformar modelos próximos ao usuário em modelos para a verificação. As regras de transformação propostas devem estar inseridas em duas cadeias de verificação formal, que utilizam as abordagens de model-checking e por equivalências de modelos. A validação da proposta é feita por intermédio da transformação de modelos e verificação das propriedades de um sistema de automação pneumática e um sistema para um misturador industrial.

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico, Programa de Pós-Graduação em Engenharia Química, Florianópolis, 2010 / Made available in DSpace on 2012-10-25T13:38:43Z (GMT). No. of bitstreams: 1 279025.pdf: 1365316 bytes, checksum: efe16b7a4367501f434279a6a62191ed (MD5) / Os ciclones, utilizados como equipamentos para troca térmica, como secadores, reatores para reações rápidas e para separação gás-sólido, apresentam na sua forma clássica uma construção cônica-cilíndrica, e têm como principais vantagens o baixo custo de construção, operação e manutenção. No passado o estudo de ciclones era basicamente experimental, resultando em correlações empíricas sem muita generalidade e dedicadas exclusivamente para a faixa de condições geométricas e operacionais analisadas nos experimentos. Com o desenvolvimento da tecnologia computacional, a modelagem numérica ganhou papel fundamental no estudo de escoamentos turbulentos multifásicos, típicos do escoamento ciclônico, destacando-se neste sentido as técnicas de CFD (Computational Fluid Dynamics), como uma ferramenta de pesquisa e desenvolvimento de projetos de engenharia. Neste trabalho é desenvolvido um estudo de modelagem numérica de ciclones a partir dos recursos de CFD, juntamente com um estudo experimental em uma Unidade Experimental de Dutos e Ciclones (UEDC) do Laboratório de Verificação e Validação da FURB. O objetivo principal é validar um modelo gás-sólido bifásico utilizado para separação ciclônica de iodato de cálcio, produzidos numa planta química de extração de iodo. Esta corroboração de modelo é realizada por comparação entre dados experimentais obtidos na UE-DC de perda de carga, eficiência global de coleta e curva de eficiência, com resultados numéricos do modelo bifásico gás-sólido, implementado no código numérico CYCLO-HEXA, dedicado exclusivamente à simulação de ciclones por técnicas de CFD. Experimentos planejados e executados no aparato experimental para diferentes velocidades de entrada e razões de carga constituem uma base empírica necessária e suficiente para estudos de validação do modelo, e de verificação do código de CFD, que permitem estudos avançados de melhoria de equipamento (reengenharia geométrica) e das condições operacionais na planta química. / The cyclones used as heat exchange equipment such as dryers, reactors for fast reactions and gas-solid separation, presented in its classic form a cone-cylindrical construction, and have as main advantages the low cost of construction, operation and maintenance. In the past the study of cyclones was basically experimental, resulting in empirical correlations without much general and dedicated exclusively to the range of geometrical and operating conditions analyzed in the experiments. With the development of computer technology, numerical modeling plays a fundamental role in the study of turbulent multiphase, typical of cyclonic flow, especially in the technical sense of CFD (Computational Fluid Dynamics), as a tool for research and development projects engineering. In this work we developed a numerical modeling study of cyclones from the resources of CFD, together with an experimental study in an Experimental Unit Pipeline and Cyclones (EU-DC). The main objective is to validate a model gas-solid two-phase used to sepa rate low-level calcium iodate, produced in a chemical plant for extraction of iodine. The corroboration of the model is performed by comparing experimental data obtained in the EU-DC loss, efficiency and overall collection efficiency curve, with numerical results of the model gas-solid two-phase, implemented in numerical code CYCLO-HEXA, devoted exclusively the simulation of cyclones using CFD techniques. Experiments planned and implemented in the experimental apparatus for different input velocities and load relations are an evidence base necessary and sufficient for studies of model validation and verification of the CFD code, which allow advanced studies for improvement of equipment (geometrical reengineering) and operating conditions in the chemical plant.

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico. Programa de Pós-graduação em Engenharia Mecânica / Made available in DSpace on 2012-10-23T13:02:41Z (GMT). No. of bitstreams: 1 258007.pdf: 3042552 bytes, checksum: 8f478cddf58140a1ad10b6bf36551049 (MD5) / O trabalho apresenta os resultados obtidos no desenvolvimento incremental de um sistema especialista protótipo, o qual tem por objetivo ser utilizado como ferramenta auxiliar na tarefa de verificação da estrutura de produto de um motor elétrico. Analisa o processo de projeto e os conceitos relacionados ao PDP (Processo de Desenvolvimento de Produtos), o qual neste trabalho está relacionado ao projeto de motores elétricos para os quais são apresentados conceitos e detalhes construtivos. Também focaliza na atividade de verificação de projeto com foco na estrutura de produto que é o principal objeto relacionado ao estudo, mostrando as conseqüências da manipulação de dados deste objeto. Aborda conceitos relacionados a sistemas especialistas e a análise de viabilidade que serviu de base para decisão de utilizar sistemas especialistas. O texto mostra o modelo de desenvolvimento incremental adotado, demonstrando a capacidade de expansão conferida ao sistema pelo uso de modelagem orientada a objetos. O trabalho também apresenta aspectos relativos à etapa de representação do conhecimento, uma proposta alternativa ao habitual processo de entrada de dados utilizada em sistemas especialistas e a ferramenta Shell utilizada na implementação. São demonstrados ainda os dados de saída resultantes da execução do sistema e o processo de verificação e validação do protótipo. O procedimento de uso do sistema adotado e os resultados obtidos por meio no número de ocorrências dos casos de erros de projeto identificados os quais permitem avaliar a qualidade dos projetos liberados e identificar a necessidade de capacitação. Finalmente são apresentadas contribuições, benefícios para a empresa, recomendações para trabalhos futuros e as conclusões finais. The work presents the results obtained from the incremental development of an expert system prototype to be used as supporting tool for the design verification of the electrical motor product structure- represented by Bill of Material. It analyzes the design process and the concepts related to PDP- Product Development Process- are also presented. The focus is the design verification, using the Bill of Material, showing the consequences of its manipulation. The work deals with expert system concepts, and the feasibility analysis used as starting point for the project. The text demonstrates the incremental development model applied, with its capacity to expand the system through the application of Object-Oriented Modeling. This project also takes into consideration the knowledge representation phase, and brings an alternative for the conventional process of interaction between the user and the prototype. The system outcomes are also discussed, with the users´ evaluation during the verification and validation phase. The results from the prototype application allow to evaluate the quality of the current design outputs and to identify the need for training. Finally, the work presents the main contributions, benefits for the company with suggestions for future projects in this research topic.

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico. Programa de Pós-graduação em Automação e Sistemas / Made available in DSpace on 2012-10-24T05:30:59Z (GMT). No. of bitstreams: 1 255209.pdf: 2427376 bytes, checksum: 5125296a32a0df94c7714b1893cb9a63 (MD5) / Analisando a história dos sistemas embarcados, podemos dividi-la em dois momentos. Em um primeiro momento, a origem dos problemas destes sistemas provinha, na grande maioria dos casos, da parte física chamada hardware. A partir dos anos 60, graças à chegada dos circuitos integrados, desenvolvidos para o Programa Espacial Americano, a parte física dos sistemas se tornou mais confiável. Nós últimos 20 anos, devido à complexidade inerente ao desenvolvimento dos softwares para sistemas embarcados, estes se tornaram a origem da maior parte dos erros. Uma das grandes dificuldades no desenvolvimento destes softwares é assegurar um funcionamento correto (de acordo com as especificações). A fim de reduzir a incidência de erros, a indústria passou a estudar o uso de métodos formais para auxiliar o desenvolvimento destes sistemas complexos. Estas técnicas auxiliam o processo decisório porque permitem afirmar antes de implementar o protótipo se uma dada especificação será cumprida ou não pelo sistema. Entretanto, a verificação formal ainda não é largamente empregada no ambiente industrial devido à dificuldade no intercâmbio de informações entre as linguagens de modelagem de alto nível (UML, AADL, SDL, etc) e as ferramentas de verificação formal. Esta dificuldade é decorrente da falta de uma semântica formal para estas linguagens de modelagem largamente utilizadas pela indústria. Além disto, cada ferramenta de verificação trabalha com formalismos matemáticos diferentes, não havendo uma fácil integração entre elas. Outro fator importante é que não podemos afirmar que existe um formalismo único capaz de atender a todas as necessidades de um sistema complexo. Isto implica que sistemas futuros vão cada vez mais requerer uma combinação de métodos baseados em modelos, tais como sistema de transição, álgebra de processos, lógica temporal, entre outros. Estas restrições impõem à indústria a necessidade de desenvolver uma ferramenta de tradução de modelos para cada par linguagem-formalismo empregado. A fim de facilitar este intercâmbio de informações entre as diferentes linguagens de modelagem e as ferramentas de verificação formais existentes - tais como TINA (Time Petri Net Analyser), CADP (Construction and Analysis of Distributed Processes), entre outras - o projeto TOPCASED (Toolkit in Open-Source for Critical Application & Systems Development) desenvolveu uma arquitetura de verificação original, que promove a transformação de modelos entre os diferentes níveis. Esta transformação é simplificada pelo advento de uma linguagem intermediária formal chamada FIACRE (Format Intermédiaire pour les Architectures de Composants Répartis Embarqués). Dentro deste contexto, as atividades desenvolvidas neste trabalho fazem parte da especificação e operacionalização da linguagem FIACRE do projeto TOPCASED. A primeira atividade apresentada neste trabalho é o estudo preliminar da tradução entre SDL e FIACRE para auxiliar na especificação da linguagem FIACRE. A segunda atividade consiste inicialmente na proposição de um esquema conceitual para a tradução de FIACRE para o formalismo matemático TTS (Sistema de Transições Temporizadas), e posteriormente na sua implementação na forma de um compilador (front-end) para a ferramenta TINA. Por último, um exemplo de verificação de sistema é apresentado com o intuito de demonstrar as vantagens das ferramentas que fazem parte do projeto TOPCASED.

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico, Programa de Pós-Graduação em Ciência da Computação, Florianópolis, 2012 / Made available in DSpace on 2013-06-25T18:37:00Z (GMT). No. of bitstreams: 1 312070.pdf: 869350 bytes, checksum: 7c9faae8b5533abbd9b63ba136b44e99 (MD5) / Este trabalho aborda duas classes de problemas enfrentados na verificação de projetos que exibem comportamentos fora de ordem, especificamente a verificação funcional de aceleradores em hardware e a verificação de consistência em sistemas de memória compartilhada. Comportamentos fora de ordem surgem quando relaxam-se restrições de precedência para aumentar a taxa de uso de componentes de hardware concorrentes e, portanto, aumentar o desempenho. Entretanto, o projeto de um sistema que apresenta comportamentos fora de ordem é suscetível a erros pelo fato de o relaxamento de ordem requerer controle sofisticado. Este trabalho compara as garantias de verificação de três classes de checkers dinâmicos para módulos com suporte a eventos fora de ordem. Comprovadamente, scoreboards relaxados podem ser construídos com plenas garantias de verificação contanto que utilizem regras de atualização baseadas na remoção de dominadores. Resultados experimentais mostram que um scoreboard relaxado assim projetado requer aproximadamente 1/2 do esforço exigido por um scoreboard convencional. Verificar a conformidade do hardware com um modelo de consistência é um problema relevante cuja complexidade depende da observabilidade dos eventos de memória. Este trabalho também descreve uma nova técnica de verificação de consistência de memória on-the-fly a partir de uma representação executável de um sistema multi-core. Para aumentar a eficiência sem afetar as garantias de verificação, são monitorados três pontos por núcleo, ao invés de um ou dois, como proposto em trabalhos correlatos anteriores. Os três pontos foram selecionados para serem altamente independentes da microarquitetura do core. A técnica usa scoreboards relaxados concorrentes para detectar violações em cada core. Para detectar violações globais, utiliza-se a ordem linear de eventos induzida por um caso de teste. Comprovadamente, a técnica não induz falsos positivos nem falsos negativos quando o caso de teste expõe um erro que afeta as sequências monitoradas, tornando-se o primeiro checker on-the-fly com plenas garantias de verificação. Resultados experimentais mostram que ele requer aproximadamente 1/4 a 3/4 do esforço global exigido por um checker post-mortem que monitora duas sequências por processador. A técnica é pelo menos 100 vezes mais rápida do que um checker que monitora uma única sequência por processador.<br> / Abstract : This work addresses two classes of problems faced when verifying designs exhibiting out-of-order behaviors, namely the functional verification of hardware accelerators and the verification of consistency in shared-memory systems. Out-of-order behaviors result from relaxing precedence constraints to increase the usage rate of concurrent hardware components and, therefore, lead to a performance improvement. However, the design of a system handling out-of-order behaviors is error prone, since order relaxation asks for sophisticated control. This work compares the verification guarantees of three classes of dynamic checkers for modules handling out-of-order behaviors. Provenly, relaxed scoreboards can be built with full verification guarantees, as far as they employ an update rule based on the removal of dominators. Experimental results show that such a relaxed scoreboard needs approximately 1/2 of the effort required by a conventional one. Verifying the hardware compliance with a consistency model is a relevant problem, whose complexity depends on the observability of memory events. This work also describes a novel on-the-fly technique for verifying memory consistency from an executable representation of a multi-core system. To increase efficiency without hampering verification guarantees, three points are monitored per core, instead of one or two, as proposed in previous related works. The points were selected to be largely independent from the core#s microarchitecture. The technique relies on concurrent relaxed scoreboards to check for consistency violations in each core. To check for global violations, it employs a linear order of events induced by a given test case. Provenly, the technique neither indicates false negatives nor false positives when the test case exposes an error that affects the sampled sequences, making it the first on-the-fly checker with full guarantees. Experimental results show that it needs approximately 1/4 to 3/4 of the overall verification effort required by a post-mortem checker sampling two sequences per processor. The technique is at least 100 times faster than a checker sampling a single sequence per processor.

Tese (doutorado) - Universidade Federal de Santa Catarina, Centro Tecnológico, Programa de Pós-Graduação em Engenharia de Automação e Sistemas, Florianópolis, 2016 / Made available in DSpace on 2016-10-19T13:26:04Z (GMT). No. of bitstreams: 0 Previous issue date: 2016Bitstream added on 2016-10-25T03:12:29Z : No. of bitstreams: 1 342327.pdf: 10243259 bytes, checksum: 34c08009c7f6079999c9bc018cac313f (MD5) / No desenvolvimento de aplicações hipermídia, o projetista pode erroneamente inserir comportamentos indesejados. Metodologias baseadas em teste ou análise de linha temporal para verificar a corretude de aplicações são limitadas, por não serem exaustivas e serem consumidoras de tempo. Outra alternativa é a utilização de metodologias baseadas em verificação formal, que permitem uma análise exaustiva e mais rápida da aplicação. A verificação formal requer que a aplicação e os comportamentos a serem verificados estejam representados em linguagens formais, de difícil aprendizagem por um projetista de aplicação hipermídia. O presente trabalho propõe uma metodologia baseada no uso de verificação formal por model-checking, a partir de uma representação da aplicação, das propriedades a serem verificadas e do diagnostico de eventuais erros, ambos em linguagens e representações de fácil uso e entendimento para o projetista destas aplicações. Essa metodologia é dividida em quatro fases: Modelagem, Transformação, Verificação e Diagnóstico/Correção. Inicialmente, o projetista codifica sua aplicação em alguma linguagem de domínio específico (por exemplo, NCL ou SMIL), e especifica os comportamentos desejados a serem verificados numa linguagem de descrição simples, proposta neste trabalho. A seguir, essas descrições das aplicações e comportamentos são transformadas, seguindo a abordagem MDE (Model Driven Engineering), nos modelos formais utilizados na verificação. Em caso de algum comportamento desejado não ser satisfeito, a ferramenta de model-checking oferece um contraexemplo que, após transformação, é apresentado na forma de uma linha de tempo, permitindo diagnosticar a origem do erro e fornecer informações para a sua correção. Para apoiar a metodologia proposta, foi construído um protótipo de um ambiente de desenvolvimento, no qual o projetista pode verificar o comportamento de sua aplicação. As avaliações da metodologia e de seu ambiente, realizadas em diversas aplicações hipermídia mostram suas potencialidades de uso para aplicações mais complexas e no caso de edição "ao vivo".<br> / Abstract : In the development of hypermedia applications, the designer can mistakenly insert undesirable behaviors. Methodologies based on tests or timeline analysis to verify the correctness of applications are limited because they are not exhaustive and are time consuming. Another alternative is the use of methodologies based on formal verification, allowing an exhaustive and more fast analysis of the application. Formal verification requires that the application and behavior to be verified are represented in formal languages, which are difficult to learn by a hypermedia application designer. This work proposes a methodology based on the use of formal verification by model-checking, from an application representation, the properties to be verified and the diagnosis of errors, both in languages and representations of easy use and understanding by designer of these applications. This methodology is divided into four phases: Modeling, Transformation, Verification and Diagnosis/Correction. Initially, the designer encodes his application in any domain specific language (eg, NCL or SMIL), and specifies the desired behaviors to be checked in a simple description language proposed in this work. Then these descriptions of applications and behaviors are transformed, following the MDE approach (Model Driven Engineering), in formal models used for verification. If some desired behavior is not satisfied, the model-checking tool provides a counterexample that, after processing, is presented as a timeline, allowing to diagnose the source of the error and provide information for its correction. To support the proposed methodology, a prototype development environment was built, in which the designer can verify the behavior of your application. Evaluations of the methodology and its environment, performed in several hypermedia applications, showed their potential of use for more complex applications and in the case of editing "live".