@MASTERSTHESIS{ 2015:749271099,
 	title = {Verifica??o de modelos aplicada ao projeto de controladores digitais implementados em processadores de ponto-fixo},
 	year = {2015},
 	url = "http://tede.ufam.edu.br/handle/tede/4984",
 	abstract = "O uso extensivo de controladores digitais implementados em ponto-fixo demandam um
 maior esfor?o para prevenir erros de projeto que aparecem no dom?nio discreto. Este trabalho
 descreve uma nova metodologia de verifica??o que emprega verifica??o de modelos limitada
 baseada em satisfa??o booleana e teorias do m?dulo da satisfatibilidade, para verificar a ocorr?ncia
 de erros de projetos em controladores digitais causados pelos efeitos da palavra finita.
 Neste trabalho, ser?o comparados os desempenhos das realiza??es na formas delta e as tradicionais
 formas diretas. Os resultados mostram que a forma delta reduz substancialmente a
 fragilidade de controladores digitais, se comparados com as formas diretas. A metodologia
 proposta ? eficiente para verificar controladores digitais do mundo real. Ela foi conclusiva em
 aproximadamente 89% dos casos de teste.",
 	publisher = {Universidade Federal do Amazonas},
 	scholl = {Programa de P?s-gradua??o em Engenharia El?trica},
 	note = {Faculdade de Tecnologia}
}