Tipo de documento:	Relatório de Pesquisa
Título:	Verificação de Controladores Digitais de Ponto-fixo usando Realizações de Formas Diretas e Deltas
Autor(a):	Vithória dos Santos Barbosa
Orientador(a):	Lucas Carvalho Cordeiro
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.
Palavras-chave:	Sistemas de controle Sistemas embarcados Verificação
Área de conhecimento - CNPQ:	ENGENHARIAS
Idioma:	pt_BR
País de publicação:	Brasil
Editor:	Universidade Federal do Amazonas
Sigla da Instituição:	UFAM
Faculdade, Instituto ou Departamento:	Faculdade de Tecnologia Faculdade de Tecnologia
Nome do programa:	PROGRAMA PIBIC 2015
Tipo de acesso:	Acesso Aberto
URI:	http://riu.ufam.edu.br/handle/prefix/5103
Data do documento:	31-jul-2016
Aparece nas coleções:	Relatórios finais de Iniciação Científica - Engenharias

Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.