Spelling suggestions: "subject:"retratibilidade"" "subject:"compatibilidade""
1 |
Avaliação de projetos de filtros digitais de ponto-fixo usando teorias do módulo da satisfatibilidadeAbreu, Renato Barbosa 17 June 2014 (has links)
Submitted by Geyciane Santos (geyciane_thamires@hotmail.com) on 2015-07-23T14:25:32Z
No. of bitstreams: 1
Dissertação - Renato Barbosa Abreu.pdf: 745859 bytes, checksum: aedacf2a1901d7a7fb83eb1ddb429e77 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-07-23T15:35:05Z (GMT) No. of bitstreams: 1
Dissertação - Renato Barbosa Abreu.pdf: 745859 bytes, checksum: aedacf2a1901d7a7fb83eb1ddb429e77 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-07-23T15:38:02Z (GMT) No. of bitstreams: 1
Dissertação - Renato Barbosa Abreu.pdf: 745859 bytes, checksum: aedacf2a1901d7a7fb83eb1ddb429e77 (MD5) / Made available in DSpace on 2015-07-23T15:38:02Z (GMT). No. of bitstreams: 1
Dissertação - Renato Barbosa Abreu.pdf: 745859 bytes, checksum: aedacf2a1901d7a7fb83eb1ddb429e77 (MD5)
Previous issue date: 2014-06-17 / Não Informada / Currently, digital filters are employed in a wide variety of signal processing applications,
using floating- and fixed-point processors. Regarding the latter, some filter implementations may be prone to errors, due to problems related to finite word-length. In particular, signal processing modules present in such realizations can produce overflows and unwanted noise caused by the quantization and round-off effects, during accumulativeaddition and multiplication operations. The present work addresses this problem and proposes a new methodology to verify digital filters, based on a state-of-the-art bounded model checker called ESBMC, which supports full C/C++ and employs satisfiabilitymodulo- theories solvers. In addition to verifying overflow and limit-cycle occurrences, the present approach can also check design properties, like stability and frequency response, as well as output errors and time constraints, based on discrete-time models implemented in C. The experiments conducted during this work show that the proposed methodology is effective, when finding realistic design errors related to fixed-point implementations of digital filters. It is worth noting that the proposed method, in addition to helping the designer to determine the number of bits for fixedpoint representations, can also aid to define details of filter realization and structure. / Atualmente, os filtros digitais são empregados em uma ampla variedade de aplicações para processamento de sinais, utilizando tanto processadores de ponto flutuante quanto de ponto fixo. No que diz respeito a este último, algumas implementações de filtro podem estar mais propensas a erros, devido a problemas relacionados com a palavra de dados de comprimento finito. Em particular, o processamento de sinais utilizando tais realizações pode produzir o problema de estouro aritmético e ruídos indesejados causados pela quantização e efeitos de arredondamento, durante operações acumulativas de adição e multiplicação. O presente trabalho aborda este problema e propõe uma nova metodologia para a verificação de filtros digitais, com base em um verificador de modelos no estado da arte, chamado ESBMC, que suporta linguagens C/C++ e emprega solucionadores baseados em teoria do módulo da satisfatibilidade. Além de verificar a ocorrência de estouro aritmético e ciclo limite, a presente abordagem também pode verificar propriedades de projeto, como estabilidade e resposta em frequência, bem como restrições temporais e erro de saída, com base em modelos de tempo discreto implementados em C. Os experimentos realizados durante este trabalho mostram que a metodologia proposta é eficaz, pois encontra erros de projeto realistas, que estão relacionados a implementações de filtros digitais em ponto fixo. Vale ressaltar que os resultados apresentados evidenciam que o método proposto, além de auxiliar o projetista a determinar o número de bits da representação de ponto fixo, também pode ajudar a definir detalhes de realização e estrutura de filtro.
|
2 |
Sobre o conceito semântico de satisfaçãoAlves, Carlos Roberto Teixeira 14 December 2015 (has links)
Made available in DSpace on 2016-04-27T17:27:13Z (GMT). No. of bitstreams: 1
Carlos Roberto Teixeira Alves.pdf: 1331347 bytes, checksum: cebe03a83120937101a3595710844df2 (MD5)
Previous issue date: 2015-12-14 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / This work aims to show the current treatment of the semantic notion of satisfiability to
the logic of the first order, the relevant problems of Tarski's solution to define this
notion - in this case, the use of infinite sequences to satisfy the formulas - and propose
an alternative to circumvent this problem. The notion established by Tarski became, in
discussions on the subject, standard solution and resulted in rich tools to work with the
languages, in particular tools such as the Theory of Models. However, from a
philosophical point of view, it is very important to broaden perspectives and look at the
problem from a new dimension. Our proposal is to avoid the counterintuitive idea of
using infinite sequences of objects to satisfy the finite formulas, knowing that these
infinite sequences are composed almost entirely of 'superfluous terms', expendable in
the process of satisfaction, but they should and are listed and indexed in the process. It
would be interesting to solve the issue involving sequences without 'superfluous terms'.
We propose a structure of first-order language that dispenses variables and constants.
The notion of satisfaction in this case is distinct, which increases the possibilities and
provides an alternative to the satisfaction of infinite sequences. In the end, we show
how our solution can produce the satisfaction of formulas of a first-order language
within a framework where satisfaction is interpreted according to certain specific
criteria and can be performed by finite sequences, differing essentially from Tarski
solution / Este trabalho tem por objetivo mostrar o tratamento atual da noção semântica de
satisfatibilidade para as lógicas de primeira ordem, os problemas relevantes da solução
de Tarski para definir essa noção no caso, o uso de sequências infinitas para a
satisfação das fórmulas , e propor uma alternativa que contorne esse problema. A
noção estabelecida por Tarski tornou-se, nas discussões a respeito do tema, a solução
padrão e resultou em ferramentas ricas para operar com as linguagens, em especial
ferramentas como a Teoria dos Modelos. No entanto, de um ponto de vista filosófico, é
sadio ampliar as perspectivas e olhar o problema sob uma dimensão nova. Nossa
proposta é superar a ideia contraintuitiva de elencarmos sequências infinitas de objetos
para satisfação das formulas finitas, sabendo que essas sequências infinitas são
compostas quase que totalmente de termos supérfluos , dispensáveis no processo de
satisfação, mas que devem e são enumerados e indexados no processo. Seria
interessante solucionar a questão envolvendo sequências sem termos supérfluos .
Proporemos uma estrutura de linguagem de primeira ordem que dispensa variáveis e
constantes. A noção de satisfação nesse caso é distinta, o que amplia as possibilidades e
fornece uma alternativa à satisfação por sequências infinitas. No fim, mostraremos
como nossa solução consegue produzir a satisfação de fórmulas de uma linguagem de
primeira ordem dentro de uma estrutura interpretada onde a satisfação ocorre segundo
certos critérios específicos e consegue ser realizada por sequências finitas, diferindo
essencialmente da solução de Tarski
|
3 |
Prova autom?tica de satisfatibilidade m?dulo teoria aplicada ao m?todo BTavares, Cl?udia Fernanda Oliveira Kiermes 27 July 2007 (has links)
Made available in DSpace on 2014-12-17T15:47:48Z (GMT). No. of bitstreams: 1
ClaudiaFCKT.pdf: 525104 bytes, checksum: 174fb60f1cf9ebfc609d837f2787b6b1 (MD5)
Previous issue date: 2007-07-27 / Este trabalho apresenta uma extens?o do provador haRVey destinada ? verifica??o de obriga??es de prova originadas de acordo com o m?todo B. O m?todo B de desenvolvimento de software abrange as fases de especifica??o, projeto e implementa??o do ciclo de vida do software. No contexto
da verifica??o, destacam-se as ferramentas de prova Prioni, Z/EVES e Atelier-B/Click n Prove. Elas descrevem formalismos com suporte ? checagem satisfatibilidade de f?rmulas da teoria axiom?tica dos conjuntos, ou seja, podem ser aplicadas ao m?todo B. A checagem de SMT consiste na checagem de satisfatibilidade de f?rmulas da l?gica de primeira-ordem livre de quantificadores dada uma teoria decid?vel. A abordagem de checagem de SMT implementada pelo provador autom?tico de teoremas haRVey ? apresentada, adotando-se a teoria
dos vetores que n?o permite expressar todas as constru??es necess?rias ?s especifica??es baseadas em conjuntos. Assim, para estender a checagem de SMT para teorias dos conjuntos destacam-se as teorias dos conjuntos de Zermelo-Frankel (ZFC) e de von Neumann-Bernays-G?del (NBG). Tendo em vista que a abordagem de checagem de SMT implementada no
haRVey requer uma teoria finita e pode ser estendida para as teorias n?odecid?veis, a teoria NBG apresenta-se como uma op??o adequada para a expans?o da capacidade dedutiva do haRVey ? teoria dos conjuntos. Assim, atrav?s do mapeamento dos operadores de conjunto fornecidos pela
linguagem B a classes da teoria NBG, obtem-se uma abordagem alternativa para a checagem de SMT aplicada ao m?todo B
|
Page generated in 0.2846 seconds