Made available in DSpace on 2014-06-12T16:01:22Z (GMT). No. of bitstreams: 2 arquivo8454_1.pdf: 1957122 bytes, checksum: 699aaa50fd31e084b62a826525a3173c (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2011 / Esta dissertação oferece contribuições para o problema de verificação de assinaturas Off-line através da criação de um classificador baseado em morfismo utilizando uma técnica de triangulação de pontos apta a gerar imagens intermediarias entre duas ou mais assinaturas. Esta técnica permite verificar a distância entre as assinaturas de uma determinada classe, objetivando discriminálas como falsas ou genuínas. Neste trabalho cinco cenários foram avaliados, em todos foram utilizadas assinaturas genuínas, falsificações simuladas e aleatórias. Do primeiro ao quarto cenários examinam-se quanto à quantidade fixa de pontos por experimento, sendo o número de pontos 10, 40, 70 e 100 respectivamente. O quinto cenário é avaliado utilizando uma quantidade variável de pontos por experimento, onde foi obtido o melhor resultado, alcançando uma taxa de erro global de 0,18. Analisou-se também o impacto que o número de assinaturas usadas como referência influencia no desempenho do sistema. Utilizou-se uma base de assinaturas para teste composta por 10 autores

O teste de software é uma atividade essencial para verificação da qualidade do produto. A grande dificuldade, porém, é a impossibilidade de se testar todos os estados que o software pode assumir, tornando-se necessário desenvolver heurísticas para atividade de teste, de forma que seja testado um subconjunto dos estados tomado como representativo. Para isto, deve-se saber avaliar o quão aceitável está o conjunto de testes. Os critérios de adequação de teste estabelecem um conjunto mínimo de regras que devem ser satisfeitas pelo conjunto de teste, de forma a analisar sua adequação, ou sua necessidade de refinamento. Dentre os critérios de adequação de teste, serão abordados neste trabalho o MC/DC (Modified Condition / Decision Coverage) e o Teste de Mutação, fazendo-se uma comparação entre ambos através da propriedade de inclusão. Pretende-se demonstrar que o Teste de Mutação, com o projeto de alguns operadores de mutação específicos, é capaz de incluir o MC/DC. A discussão é trazida para o nível dos requisitos sob a forma de modelos, que antecipa a utilização dos critérios para uma etapa anterior à geração de código no desenvolvimento de software. Será desenvolvido um algoritmo gerador de mutantes em modelos gerados na ferramenta SCADE de tal forma que ao matarem-se todos os modelos mutantes, automaticamente o MC/DC no modelo original será satisfeito.

Este trabalho tem como objetivo a análise da aplicação de métodos formais para a modelagem e verificação de produtos de software embarcado para aplicações aeroespaciais de tempo-real. Como abordagem para modelagem, utilizam-se autômatos temporizados e a ferramenta UPPAAL. A verificação do modelo construído é realizada por meio da abordagem de model-checking, utilizando um conjunto de propriedades definidas em CTL que refletem os requisitos do sistema em análise. Particular ênfase é dada ao problema de verificação de requisitos de tempo no sistema em análise. Para tanto, a metodologia proposta inclui a modelagem não apenas do aplicativo de software mas também do sistema operacional que gerencia os diversos processos executados pelo software. Como estudo de caso utiliza-se o computador de bordo de um simulador de satélite com um grau de liberdade. Este estudo de caso inclui a determinação dos tempos utilizados para execução do software aplicativo e dos tempos utilizados pelo sistema operacional. Além da verificação dos requisitos de tempo do sistema, o estudo de caso apresenta uma análise de sensibilidade destes requisitos frente à variação de alguns parâmetros do sistema. Baseado nos resultados do estudo de caso, apontam-se as vantagens e limitações do uso da abordagem de model checking para verificação de sistemas de tempo real para aplicações aeroespaciais.

Este trabalho propõe e avalia a aplicação da técnica de verificação model checking no desenvolvimento de software embarcado de satélites universitários. Inicialmente, apresenta uma revisão do cenário atual de projetos de satélites universitários, com foco no computador de bordo e a adoção de normas para este subsistema. Esta revisão aponta que os satélites universitários tendem a adotar estratégias simples e de baixo custo para garantir dependabilidade, o que torna o uso de model checking uma solução atrativa, viável e factível para verificação da especificação de software embarcado crítico destes satélites. Como estudo de caso, utiliza-se a ferramenta UPPAAL, baseada em autômatos temporizados, para verificação da especificação de software do módulo de comunicação (CM) do computador de bordo do satélite universitário ITASAT. Este módulo executa programas sequenciais que contemplam: recepção de telecomando, execução de comandos diretos, verificação dos principais canais e envio de telemetria. A primeira etapa do processo de aplicação de model checking consistiu na modelagem, de forma isolada, de cada um dos dois submódulos do CM. Para cada modelo, foram feitas verificações de propriedades básicas e dos requisitos de software. Foras discutidas estratégias práticas para contornar o problema de explosão de número de estados. Numa segunda etapa, os modelos dos dois submódulos foram integrados em um único modelo. Para o modelo integrado, foram verificadas as propriedades de alcançabilidade, ausência de deadlock e propriedades referentes a interação entre os módulos. Apesar das restrições de comandos disponíveis, devido ao problema de explosão de estados, foram criados cenários de verificação para observar a relação entre módulos. Ao final, conclui-se que a utilização do model checking permitiu a identificação de erros e de oportunidades de melhoria na especificação de requisitos e que é uma solução viável para atender a proposta de satélites universitários.

O domínio de sistema de software crítico embarcado requer atividades de Engenharia Reversa de Software especializadas para atender características típicas a esse tipo de sistema. A Engenharia Reversa de Software para sistemas de software críticos embarcados não tem focado na análise temporal de tais sistemas. Um dos desafios é a construção de um modelo para análise com detalhes suficientes para expressar as propriedades temporais que são de interesse de uma atividade de Engenharia Reversa de Software. Este trabalho propõe uma abordagem de Engenharia Reversa de Software para sistema de software crítico embarcado visando propiciar um entendimento dos aspectos temporais e segurança do software por meio de um modelo formal, a fim de prover o entendimento completo de tais aspectos. A solução é essencialmente baseada nas atividades de verificação formal de software e modelo e em uma base de conhecimento para armazenar os resultados dessas atividades. Os resultados da aplicação da abordagem em um software aeroespacial sugerem que a abordagem é viável de ser executada e correta ao atingir seu objetivo principal, que é aumentar a compreensão geral do sistema tanto para manutenção, evolução bem como para desenvolvimento de software novo.

Nos ambientes de desenvolvimento de sistemas integrados da atualidade, os requisitos dos sistemas devidos ao alto grau de funcionalidades incorporadas vêm-se incrementando, gerando uma alta complexidade nos projetos. Isto traz como consequência o aumento na quantidade de ciclos dentro do fluxo de projeto. Uma solução tem sido o uso de blocos IP para acelerar o desenvolvimento. Entretanto, para garantir um grau elevado de confiabilidade destes componentes, os processos de verificação devem comprovar que todas as propriedades do circuito estejam sendo cumpridas. Uma das técnicas utilizadas para isto é verificação funcional por simulação, que procura explorar, através da injeção de vetores de teste, a maior porção possível de todo o espaço de estados do circuito. Quanto maior o número de estados possíveis, maior o número de vetores de testes que devem ser inseridos. Portanto, o número de vetores de teste deve ser reduzido de forma considerável, entretanto, por este fato, métricas para determinar a completeza do processo de verificação, definidas como modelos de cobertura, têm sido necessárias. As métricas de cobertura são estabelecidas segundo as estratégias de observação do projeto sob verificação, DUV, sendo bastante comum na indústria a de caixa preta que tem como objetivo a estimulação das entradas e a observação dos eventos de saída do DUV. Neste caso, para determinar se o sistema cumpre com as especificações, o engenheiro de verificação, deve definir os eventos à saída que considera relevantes e as métricas para determinar a quantidade de vezes que devem ser observadas. Este tipo de modelagem é conhecido como cobertura por itens. A quantidade de itens e os eventos a serem observados podem ser dfinidos pelo conhecimento especialista, dos engenheiros de verificação ou, para simplificar esta tarefa, uma distribuição uniforme é adotada. Como estas formas de modelagem não abstraem todas as propriedades do circuito, o perfil da distribuição de valores dos eventos (parâmetros) escolhidos, em geral, não estão correlacionados com o perfil real verficado durante a execução dos testbenches , tendo como consequência o aumento dos tempos de simulação. Para tratar do problema acima, o presente trabalho tem como objetivo geral o desenvolvimento de uma metodologia para obter um modelo de cobertura de saída que apresente um perfil de distribuição semelhante ao real e que, assim, assista o engenheiro de verificação na seleção dos pontos ou intervalos de saída de interesse, adicionado-os às decisões derivadas de seu conhecimento especialista. Pela metodologia utilizada, encontra-se a(s) equação(ões) que define(m) a(s) saída(s) do circuito sob verificação e, a partir destas, a distribuição probabilística por evento observável. No centro da metodologia está a ferramenta PrOCov (Probabilistic Output Coverage), projetada com os objetivos acima. A metodologia e a ferramenta foram testadas com alguns exemplos de circuitos, modelos em alto nível do filtro FIR, do processador FFT e do filtro Elliptic, todos descritos em SystemC. Nos três casos testados, o PrOCov encontrou satisfatoriamente os respectivos perfis de saída. Estes foram comparados com os perfis obtidos por simulação, mostrando que uma excelente precisão pode ser obtida; apenas pequenas variações foram encontradas devidas a erros de aproximação. Também variações de precisão e tempo de simulação em função da resolução dos parâmetros de saída (eventos) foram analisadas nesta dissertação. / In current integrated system development environments, the requirements for the design of multi-function systems have increased constantly. Consequently, the number of iterations in the design flow has also grown. A solution for this problem has been the use of IP-cores to speed up the hardware development. However, to guarantee high level of reliability for these components, the verification process has to be kept strict in other to prove if the all system properties have been satisfied. The mainstream technique that has been used in the industry for the verification process is the dynamic functional verification. It aims to explore, by test vector injection, all the state space of the circuit. The higher the number of possible states, the higher the number of test vectors to be inserted. Therefore, the number of test vectors must be kept as low as possible. Due to that, completion and sufficiency metrics, identified as the coverage model, should be carefully defined. The coverage metrics are established according the observation strategies of the design under verification, DUV, where the black box approach is very common in the industry, being aimed at the stimulation of the inputs and observing the events of the DUV output. To determine whether the system meets the specifications, the verification engineer must define the events (s)he considers relevant at the output and the metrics used to determine the amount of times that the results must be observed. This type of modeling is known as item coverage. The amount of items and events to be observed may be defined by the experience of the engineer, but in most cases, to simplify this task, a uniform distribution is adopted. Those forms of modeling do not abstract the functionality of the circuit, then, the probability distribution of the chosen events is uncorrelated to the real simulated distribution, when the testbenchs are implemented. Therefore, the resulting simulation time increases. To solve the problem that is mentioned above, this work aims the development of a methodology to compute the output coverage, which should be similar to the real output value distribution and thus assist the engineer in the selection of the proper check points or output ranges of interest, by adding them to the decisions derived from his(her) knowledge. This methodology finds the equations that represent the outputs of the DUV and, from them, it computes the output probabilistic distribution. At the core of this methodology is the PrOCov (Probabilistic Output Coverage) tool, which was developed with the goals above. Both methodology and tool were tested with three circuits described in high level language, the FIR filter, FFT processor and Elliptic filter, written in SystemC. In all three cases, PrOCov presented a satisfactorily output distribution. Excellent precision could be achieved by the results, with only small variations found due to approximation errors. Also variations of accuracy and simulation time due to different resolutions of the output parameters (events) were analyzed in this dissertation.

MARINHO, Fabiana Gomes. PRECISE - Um processo de verificação formal para modelos de características de aplicações móveis e sensíveis ao contexto. 2012. 181 f. Tese (Doutorado em ciência da computação)- Universidade Federal do Ceará, Fortaleza-CE, 2012. / Submitted by Elineudson Ribeiro (elineudsonr@gmail.com) on 2016-07-12T19:42:02Z No. of bitstreams: 1 2012_tese_fgmarinho.pdf: 5103390 bytes, checksum: dd5da728cc7af5f3e122c8c7afaf49aa (MD5) / Approved for entry into archive by Rocilda Sales (rocilda@ufc.br) on 2016-07-25T11:39:31Z (GMT) No. of bitstreams: 1 2012_tese_fgmarinho.pdf: 5103390 bytes, checksum: dd5da728cc7af5f3e122c8c7afaf49aa (MD5) / Made available in DSpace on 2016-07-25T11:39:31Z (GMT). No. of bitstreams: 1 2012_tese_fgmarinho.pdf: 5103390 bytes, checksum: dd5da728cc7af5f3e122c8c7afaf49aa (MD5) Previous issue date: 2012 / SPLc have been used to develop different types of applications, including the ones that run on mobile devices and are able to adapt when the context elements in which they are located change. These applications can change due to variations in their execution environment and inconsistent adaptations can occur, compromising the expected behavior. Then there is a need for creating a verification process to check the correctness and consistency of these SPLs as well as to check the correctness of both derived products and adapted products from these SPLs. Thus, this work proposes PRECISE - A Formal Verification Process for Feature Models of Mobile and Context-Aware Applications. PRECISE helps to identify defects in the variability modeling of an SPL for mobile and context-aware applications, minimizing problems that can take place during the execution of products generated from this SPL. It is worth noting that PRECISE is defined based on a formal specification and a set of well-formedness properties developed using First-Order Logic, which are prerequisites for the achievement of an unambiguous variability modeling. To evaluate PRECISE, a validation is performed from the formal specification and well-formedness properties defined in the process. This validation intends to show that PRECISE is able to identify defects, anomalies and inconsistencies in a variability model of an SPL for mobile and context-aware applications. In this validation, five different techniques are used: UML Profile, OCL, Propositional Logic, Prolog and Simulation. While minimizing the defects and inconsistencies in the variability models of an SPL, PRECISE still benefits from the generality and flexibility intrinsic to the formal notation used in its specification. / As LPSs, além do seu uso em aplicações tradicionais, têm sido utilizadas no desenvolvimento de aplicações que executam em dispositivos móveis e são capazes de se adaptarem sempre que mudarem os elementos do contexto em que estão inseridas. Essas aplicações, ao sofrerem alterações devido a mudanças no seu ambiente de execução, podem sofrer adaptações inconsistentes e, consequentemente, comprometer o comportamento esperado. Por esse motivo, é essencial a criação de um processo de verificação que consiga checar a corretude e a consistência dessas LPSS, bem como checar a corretude tanto dos produtos derivados como dos produtos adaptados dessas LPSs. Sendo assim, nesta tese de doutorado é proposto o PRECISE - um Processo de Verificação Formal para Modelos de Características de Aplicações Móveis e Sensíveis ao Contexto. O PRECISE auxilia na identificação de defeitos na modelagem da variabilidade de uma LPS para aplicações móveis e sensíveis ao contexto e, assim, minimiza problemas que ocorreriam durante a execução dos produtos gerados a partir dessa LPS. É importante ressaltar que o PRECISE é definido com base em uma especificação formal e em um conjunto de propriedades de boa formação elaborados usando Lógica de Primeira Ordem. Essa especificação é um pré-requisito para a realização de uma modelagem da variabilidade sem ambiguidades. Para avaliar o PRECISE, uma validação é realizada a partir da especificação formal e das propriedades de boa formação definidas no processo. Essa validação tem como objetivo mostrar que o PRECISE consegue identificar defeitos, anomalias e inconsistências existentes em um modelo de variabilidades de uma LPS para aplicações móveis e sensíveis ao contexto. Nessa validação, cinco técnicas diferentes são utilizadas: Perfil UML, OCL, Lógica Proposicional, Prolog e Simulação. Além de minimizar os defeitos e inconsistências dos modelos de variabilidades das LPSs, o PRECISE ainda se beneficia da generalidade e flexibilidade intrínsecas à notação formal usada na sua especificação.

Submitted by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2018-03-21T17:40:38Z No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação_Raimundo W. R. Melo.pdf: 1511352 bytes, checksum: 35f1429da9fc237f23a6e983f4c6abd9 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2018-03-21T17:40:50Z (GMT) No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação_Raimundo W. R. Melo.pdf: 1511352 bytes, checksum: 35f1429da9fc237f23a6e983f4c6abd9 (MD5) / Made available in DSpace on 2018-03-21T17:40:50Z (GMT). No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação_Raimundo W. R. Melo.pdf: 1511352 bytes, checksum: 35f1429da9fc237f23a6e983f4c6abd9 (MD5) Previous issue date: 2017-08-10 / FAPEAM - Fundação de Amparo à Pesquisa do Estado do Amazonas / The use of embedded systems, i.e., computer systems focused on performing specific functions in larger (electronic or mechanical) systems, has been growing lately, and ensuring the robustness of such systems has become increasingly important. There are several techniques to ensure that a system is released without errors. In particular, formal verification of programs is proving itself to be effective in the search for failures. In this work, an induction-proof algorithm is described, which combines k-induction and invariants to verify and refute safety properties in embedded ANSI-C software. Moreover, the proposed k-induction-based approach infers invariants in the program to assist in verification tasks, using constraint refinement (i.e., polyhedral) to specify pre- and post-conditions. We adopted two invariant generators to produce such and feed the k-induction algorithm, which is implemented in the Efficient SMT-Based Context-Bounded Model Checker tool. Public benchmarks were used to assess the effectiveness of our approach. In addition, a comparison to other state-of-the-art verification tools using a set of benchmarks from the International Competition for Software Verification in addition to embedded systems applications. Experimental results have shown that the proposed approach, with and without invariants, can verify a wide variety of safety properties in programs with loops and embedded software from telecommunications, control systems, and medical domains. / O uso de sistemas embarcados, sistemas computacionais especializados para execução em sistemas eletrônicos ou mecânicos tem crescido de forma vertiginosa devido a utilização cada vez mais intensa de sensores, interfaces de rede e protocolos de comunicação em diversas áreas. Por isso, é cada vez mais importante garantir a robustez desses sistemas, uma vez que estão se tornando mais complexos e integrados. Existem várias técnicas para garantir que um sistema seja entregue ao cliente sem erros, em particular, a verificação formal dos programas tem se revelado eficaz na busca de falhas. Neste trabalho é descrito um algoritmo de indução matemática conhecido como k-induction combinado ao uso de invariantes para verificar e refutar propriedades de segurança em programas desenvolvidos na linguagem ANSI-C. Em particular, a abordagem proposta infere invariantes no programa para auxiliar na verificação de programas ANSI-C através da técnica de indução matemática através do refinamento de restrição (i.e, poliédrico) para especificar pré- e pós-condições. No método proposto, adotamos dois geradores de invariantes para produzir e alimentar o algoritmo de indução matemática o qual é implementado na ferramenta Efficient SMT-Based Context-Bounded Model Checker. A motivação para a combinação de invariantes com o algoritmo de indução matemática é fechar um gap na verificação formal de programas que possuam variáveis globais, além de programas com loops que possuem desvios condicionais e o número de iterações é desconhecido. PIPS e PAGAI são as ferramentas utilizadas para analisar o código e produzir invariantes indutivas responsáveis por guiar o algoritmo de indução matemática na verificação do benchmark, sendo este o principal desafio do método proposto. Para avaliar a eficácia da abordagem proposta neste trabalho, além de aplicações de Sistemas Embarcados foram utilizados benchmarks públicos disponibilizados pela Competição Internacional de Verificação de Software onde participam Universidades, pesquisadores, estudandantes de doutorado de várias partes do mundo, e fornece amplo conjunto de casos de teste para verificação. Além disso, foram utilizadas ferramentas estado-da-arte para a comparação dos resultados e, assim mensurar a eficácia do método proposto. Os resultados experimentais foram positivos e mostraram que o algoritmo de indução matemática com invariantes pode verificar uma grande variedade de propriedades de segurança em programas com loops e aplicações de sistemas embarcados de telecomunicações, sistemas de controle e dispositivos médicos.

Nos ambientes de desenvolvimento de sistemas integrados da atualidade, os requisitos dos sistemas devidos ao alto grau de funcionalidades incorporadas vêm-se incrementando, gerando uma alta complexidade nos projetos. Isto traz como consequência o aumento na quantidade de ciclos dentro do fluxo de projeto. Uma solução tem sido o uso de blocos IP para acelerar o desenvolvimento. Entretanto, para garantir um grau elevado de confiabilidade destes componentes, os processos de verificação devem comprovar que todas as propriedades do circuito estejam sendo cumpridas. Uma das técnicas utilizadas para isto é verificação funcional por simulação, que procura explorar, através da injeção de vetores de teste, a maior porção possível de todo o espaço de estados do circuito. Quanto maior o número de estados possíveis, maior o número de vetores de testes que devem ser inseridos. Portanto, o número de vetores de teste deve ser reduzido de forma considerável, entretanto, por este fato, métricas para determinar a completeza do processo de verificação, definidas como modelos de cobertura, têm sido necessárias. As métricas de cobertura são estabelecidas segundo as estratégias de observação do projeto sob verificação, DUV, sendo bastante comum na indústria a de caixa preta que tem como objetivo a estimulação das entradas e a observação dos eventos de saída do DUV. Neste caso, para determinar se o sistema cumpre com as especificações, o engenheiro de verificação, deve definir os eventos à saída que considera relevantes e as métricas para determinar a quantidade de vezes que devem ser observadas. Este tipo de modelagem é conhecido como cobertura por itens. A quantidade de itens e os eventos a serem observados podem ser dfinidos pelo conhecimento especialista, dos engenheiros de verificação ou, para simplificar esta tarefa, uma distribuição uniforme é adotada. Como estas formas de modelagem não abstraem todas as propriedades do circuito, o perfil da distribuição de valores dos eventos (parâmetros) escolhidos, em geral, não estão correlacionados com o perfil real verficado durante a execução dos testbenches , tendo como consequência o aumento dos tempos de simulação. Para tratar do problema acima, o presente trabalho tem como objetivo geral o desenvolvimento de uma metodologia para obter um modelo de cobertura de saída que apresente um perfil de distribuição semelhante ao real e que, assim, assista o engenheiro de verificação na seleção dos pontos ou intervalos de saída de interesse, adicionado-os às decisões derivadas de seu conhecimento especialista. Pela metodologia utilizada, encontra-se a(s) equação(ões) que define(m) a(s) saída(s) do circuito sob verificação e, a partir destas, a distribuição probabilística por evento observável. No centro da metodologia está a ferramenta PrOCov (Probabilistic Output Coverage), projetada com os objetivos acima. A metodologia e a ferramenta foram testadas com alguns exemplos de circuitos, modelos em alto nível do filtro FIR, do processador FFT e do filtro Elliptic, todos descritos em SystemC. Nos três casos testados, o PrOCov encontrou satisfatoriamente os respectivos perfis de saída. Estes foram comparados com os perfis obtidos por simulação, mostrando que uma excelente precisão pode ser obtida; apenas pequenas variações foram encontradas devidas a erros de aproximação. Também variações de precisão e tempo de simulação em função da resolução dos parâmetros de saída (eventos) foram analisadas nesta dissertação. / In current integrated system development environments, the requirements for the design of multi-function systems have increased constantly. Consequently, the number of iterations in the design flow has also grown. A solution for this problem has been the use of IP-cores to speed up the hardware development. However, to guarantee high level of reliability for these components, the verification process has to be kept strict in other to prove if the all system properties have been satisfied. The mainstream technique that has been used in the industry for the verification process is the dynamic functional verification. It aims to explore, by test vector injection, all the state space of the circuit. The higher the number of possible states, the higher the number of test vectors to be inserted. Therefore, the number of test vectors must be kept as low as possible. Due to that, completion and sufficiency metrics, identified as the coverage model, should be carefully defined. The coverage metrics are established according the observation strategies of the design under verification, DUV, where the black box approach is very common in the industry, being aimed at the stimulation of the inputs and observing the events of the DUV output. To determine whether the system meets the specifications, the verification engineer must define the events (s)he considers relevant at the output and the metrics used to determine the amount of times that the results must be observed. This type of modeling is known as item coverage. The amount of items and events to be observed may be defined by the experience of the engineer, but in most cases, to simplify this task, a uniform distribution is adopted. Those forms of modeling do not abstract the functionality of the circuit, then, the probability distribution of the chosen events is uncorrelated to the real simulated distribution, when the testbenchs are implemented. Therefore, the resulting simulation time increases. To solve the problem that is mentioned above, this work aims the development of a methodology to compute the output coverage, which should be similar to the real output value distribution and thus assist the engineer in the selection of the proper check points or output ranges of interest, by adding them to the decisions derived from his(her) knowledge. This methodology finds the equations that represent the outputs of the DUV and, from them, it computes the output probabilistic distribution. At the core of this methodology is the PrOCov (Probabilistic Output Coverage) tool, which was developed with the goals above. Both methodology and tool were tested with three circuits described in high level language, the FIR filter, FFT processor and Elliptic filter, written in SystemC. In all three cases, PrOCov presented a satisfactorily output distribution. Excellent precision could be achieved by the results, with only small variations found due to approximation errors. Also variations of accuracy and simulation time due to different resolutions of the output parameters (events) were analyzed in this dissertation.

Submitted by Johnny Rodrigues (johnnyrodrigues@ufcg.edu.br) on 2018-08-27T17:42:49Z No. of bitstreams: 1 HELDER FERNANDO DE ARAUJO OLIVEIRA - DISSERTAÇÃO PPGCC 2010..pdf: 2110687 bytes, checksum: 5d2a2c0f6c5039c3f21dd8219d20f122 (MD5) / Made available in DSpace on 2018-08-27T17:42:49Z (GMT). No. of bitstreams: 1 HELDER FERNANDO DE ARAUJO OLIVEIRA - DISSERTAÇÃO PPGCC 2010..pdf: 2110687 bytes, checksum: 5d2a2c0f6c5039c3f21dd8219d20f122 (MD5) Previous issue date: 2010-06-16 / O processo de desenvolvimento de um circuito digital complexo pode ser composto por diversas etapas. Uma delas é a verificação funcional. Esta etapa pode ser considerada uma das mais importantes, pois tem como objetivo demonstrar que as funcionalidades do circuito a ser produzido estão em conformidade com a sua especificação. Porém, além de ser uma fase com grande consumo de recursos, a complexidade da verificação funcional cresce diante da complexidade do hardware a ser verificado. Desta forma, o uso de uma metodologia de verificação funcional eficiente e de ferramentas que auxiliem o engenheiro de verificação funcional são de grande valia. Neste contexto, este trabalho realiza uma reformulação da metodologia de verificação funcional VeriSC, originando uma nova metodologia, denominada BVM (Brazil-IP Verification Methodology). VeriSC é implementada em SystemC e utiliza as bibliotecas SCV (SystemC Verification Library) e BVE (Brazil-IP Verification Extensions), enquanto BVM é implementada em SystemVerilog e baseada em conceitos e biblioteca de OVM (Open Verification Methodology). Além disto, este trabalho visa a adequação da ferramenta de apoio à verificação funcional eTBc (Easy Testbench Creator) para suportar BVM. A partir do trabalho realizado, é possível constatar, mediante estudos de caso no âmbito do projeto Brazil-IP, que BVM traz um aumento da produtividade do engenheiro de verificação na realização da verificação funcional, em comparação à VeriSC / The development process of a complex digital circuit can consist of several stages. One of them is the functional verification. This stage can be considered one of the most important because it aims to demonstrate that a circuit functionality to be produced is in accordance with its specification. However, besides being a stage with large consumption of resources, the complexity of functional verification grows according to the complexity of the hardware to be verified. Thus, the use of an effective functional verification methodology and tools to help engineer the functional verification are of great value. Within this context, this work proposes a reformulation of the functional verification methodology VeriSC, resulting in a new methodology called BVM (Brazil-IP Verification Methodology). VeriSC is implemented in SystemC and uses the SCV (SystemC Verification Library) and BVE (Brazil-IP Verification Extensions) libraries, while BVM is implemented and based on SystemVerilog and OVM (Open Verification Methodology) concepts and library. Furthermore, this study aims the adequacy of the functional verification tool eTBc (testbench Easy Creator), to support BVM. From this work it can be seen, based on case studies under the Brazil-IP project, that BVM increase the productivity of the engineer in the functional verification stage when compared to VeriSC.