Submitted by Bianca Neves (oliveirabia1@ymail.com) on 2016-04-20T19:50:59Z
No. of bitstreams: 1
Dissertação -Hussama Ibrahim Ismail.pdf: 7224207 bytes, checksum: 580676e0f2285e31f50bddf1814c3d9b (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-04-27T18:31:16Z (GMT) No. of bitstreams: 1
Dissertação -Hussama Ibrahim Ismail.pdf: 7224207 bytes, checksum: 580676e0f2285e31f50bddf1814c3d9b (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2016-04-27T20:06:56Z (GMT) No. of bitstreams: 1
Dissertação -Hussama Ibrahim Ismail.pdf: 7224207 bytes, checksum: 580676e0f2285e31f50bddf1814c3d9b (MD5) / Made available in DSpace on 2016-04-27T20:06:56Z (GMT). No. of bitstreams: 1
Dissertação -Hussama Ibrahim Ismail.pdf: 7224207 bytes, checksum: 580676e0f2285e31f50bddf1814c3d9b (MD5)
Previous issue date: 2015-11-11 / Não informada / The extensive use of fixed-point digital controllers demands a growing effort to prevent
design errors that appear in discrete-time domain. The present work describes a novel
verification methodology, which employs bounded model checking based on boolean satisfiability and satisfiability modulo theories to verify the occurrence of design errors, due to the finite word-length format, in fixed-point digital controllers. Here, the performance of digital controllers realizations that use delta operators are compared to those that use traditional direct forms. Experimental results show that the delta-form realization substantially reduces the digital controllers’ fragility when compared to the direct-form realization. Additionally, the proposed methodology is very effective and efficient to verify real-world digital controllers, where conclusive results are obtained in nearly 89% of the benchmarks. / 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.
| Identifer | oai:union.ndltd.org:IBICT/oai:http://localhost:tede/4984 |
| Date | 11 November 2015 |
| Creators | Ismail, Hussama Ibrahim |
| Contributors | Cordeiro, Lucas Carvalho, Cordeiro, Lucas Carvalho, de Lima Filho, Eddie Batista, D'Angelo, Marcos Flávio Silveira Vasconcelos |
| Publisher | Universidade Federal do Amazonas, Programa de Pós-graduação em Engenharia Elétrica, UFAM, Brasil, Faculdade de Tecnologia |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Format | application/pdf |
| Source | reponame:Biblioteca Digital de Teses e Dissertações da UFAM, instname:Universidade Federal do Amazonas, instacron:UFAM |
| Rights | info:eu-repo/semantics/openAccess |
| Relation | -161377036298529205, 600, 600, -5930111888266832212 |
Page generated in 0.0018 seconds