metadata.dc.type:	Relatório de Pesquisa
Title:	Verificação de Controladores Digitais de Ponto-fixo usando Realizações de Formas Diretas e Deltas
metadata.dc.creator:	Vithória dos Santos Barbosa
metadata.dc.contributor.advisor1:	Lucas Carvalho Cordeiro
metadata.dc.description.resumo:	Controles digitais são amplamente utilizados pela comunidade de engenharia de controle por causa das várias vantagens sobre os controladores analógicos, tais como a melhoria da confiabilidade, sensibilidade, flexibilidade e custo. Entretanto, existem algumas desvantagens em usar controladores digitais, por exemplo, erros que são introduzidos durante o processo de quantização. Neste contexto, existem algumas iniciativas para resolver os problemas que aparecem no domínio de tempo discreto; e em particular, problemas relacionados com os efeitos do comprimento de palavra finita (FWL). De acordo com a escolha do hardware, o formato e a aritmética usados para representar e manipular os números podem mudar (por exemplo, número de bits, aritmética de ponto fixo ou flutuante). Essas representações influenciam diretamente no correto funcionamento do controlador digital. O cenário mencionado acima, requer uma melhor compreensão e manipulação dos problemas típicos na realização de controles digitais para que efeitos de quantização e FWL possam ser potencialmente reduzidos ao projetar um controlador digital. Diversos fatores podem influenciar, intensificar ou atenuar esses efeitos (por exemplo, através da utilização de estruturas realizadas tais como as formas direta e a delta, bem como a definição de número de bits e a taxa de amostragem). A possível influência que esses efeitos trazem são importantes para a estabilidade e consequentemente, o correto funcionamento dos controladores digitais. Para evitar a degradação do desempenho, engenheiros de controle geralmente investem tempo e esforço durante a fase de projeto, resolvendo problemas causados por efeitos do FWL com soluções mais robustas e árduas. Estudos anteriores propõem escalas apropriadas usando medidas apropriadas. Outros desenvolvem diferentes metodologias para estimar o comprimento da palavra ideal, para evitar efeitos do FWL. Existem algumas iniciativas que propõem controladores mais complexos para manter o desempenho dentro de um erro ou incerteza vinculada aos limites (por exemplo, controladores robustos e não frágeis). Ferramentas de verificação automáticas também foram aplicadas para encontrar erros de projeto no sistema de tempo discreto. Entretanto, ainda há uma lacuna na verificação formal de sistemas embarcados; e em particular os controladores digitais. Diferente de outros trabalhos relacionados, esse projeto de pesquisa apresentará uma nova metodologia para verificar formalmente a ocorrência de erros de projeto na realização de controladores digitais. Em especial, a verificação de modelo limitada baseada nas teorias do módulo da satisfatibilidade é usada para verificar cinco tipos de propriedades, que incluem estouro aritmético, ciclo limite, restrições temporais, estabilidade, e fase mínima. Adicionalmente, seis diferentes realizações serão consideradas, nas quais incluem três formas direta e três formas delta.
Keywords:	Sistemas de controle Sistemas embarcados Verificação
metadata.dc.subject.cnpq:	ENGENHARIAS
metadata.dc.language:	pt_BR
metadata.dc.publisher.country:	Brasil
Publisher:	Universidade Federal do Amazonas
metadata.dc.publisher.initials:	UFAM
metadata.dc.publisher.department:	Faculdade de Tecnologia Faculdade de Tecnologia
metadata.dc.publisher.program:	PROGRAMA PIBIC 2015
metadata.dc.rights:	Acesso Aberto
URI:	http://riu.ufam.edu.br/handle/prefix/5103
Issue Date:	31-Jul-2016
Appears in Collections:	Relatórios finais de Iniciação Científica - Engenharias

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.