Submitted by Erickson Alves (erickson.higor@gmail.com) on 2018-11-22T22:41:27Z
No. of bitstreams: 1
capa de aprovação de Erickson.pdf: 159098 bytes, checksum: 53aadfbcf021e94fca0a6734d55714f0 (MD5) / Approved for entry into archive by PPGEE Engenharia Elétrica (mestrado_engeletrica@ufam.edu.br) on 2018-11-23T12:51:53Z (GMT) No. of bitstreams: 1
capa de aprovação de Erickson.pdf: 159098 bytes, checksum: 53aadfbcf021e94fca0a6734d55714f0 (MD5) / Rejected by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br), reason: O depósito está incompleto. É necessário fazer o upload da Dissertação, da Carta de Encaminhamento assinada pelo orientador.
Segue orientações no link http://biblioteca.ufam.edu.br/servicos/teses-e-dissertacoes
Dúvidas? ddbc@ufam.edu.br on 2018-11-23T14:01:34Z (GMT) / Submitted by Erickson Alves (erickson.higor@gmail.com) on 2018-11-29T00:18:47Z
No. of bitstreams: 3
capa de aprovação de Erickson.pdf: 159098 bytes, checksum: 53aadfbcf021e94fca0a6734d55714f0 (MD5)
carta_encaminhamento.pdf: 373281 bytes, checksum: 057300b8bfec478dcee8902fab4d381b (MD5)
dissertação.pdf: 627984 bytes, checksum: cfec6a01af6780eda1337a48143def43 (MD5) / Approved for entry into archive by PPGEE Engenharia Elétrica (mestrado_engeletrica@ufam.edu.br) on 2018-11-29T13:12:34Z (GMT) No. of bitstreams: 3
capa de aprovação de Erickson.pdf: 159098 bytes, checksum: 53aadfbcf021e94fca0a6734d55714f0 (MD5)
carta_encaminhamento.pdf: 373281 bytes, checksum: 057300b8bfec478dcee8902fab4d381b (MD5)
dissertação.pdf: 627984 bytes, checksum: cfec6a01af6780eda1337a48143def43 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2018-11-29T14:29:30Z (GMT) No. of bitstreams: 3
capa de aprovação de Erickson.pdf: 159098 bytes, checksum: 53aadfbcf021e94fca0a6734d55714f0 (MD5)
carta_encaminhamento.pdf: 373281 bytes, checksum: 057300b8bfec478dcee8902fab4d381b (MD5)
dissertação.pdf: 627984 bytes, checksum: cfec6a01af6780eda1337a48143def43 (MD5) / Made available in DSpace on 2018-11-29T14:29:30Z (GMT). No. of bitstreams: 3
capa de aprovação de Erickson.pdf: 159098 bytes, checksum: 53aadfbcf021e94fca0a6734d55714f0 (MD5)
carta_encaminhamento.pdf: 373281 bytes, checksum: 057300b8bfec478dcee8902fab4d381b (MD5)
dissertação.pdf: 627984 bytes, checksum: cfec6a01af6780eda1337a48143def43 (MD5)
Previous issue date: 2018-09-14 / Este trabalho descreve uma nova abordagem para localizar falhas em programas concorrentes, a qual é baseada em técnicas de verificação de modelos limitada e sequencialização. A principal novidade dessa abordagem é a ideia de reproduzir um comportamento defeituoso em uma versão sequencial do programa concorrente. De forma a apontar linhas defeituosas, analizam-se os contraexemplos gerados por um verificador de modelos para o programa sequencial instrumentado e procura-se um valor para uma variável de diagnóstico, o qual corresponde a linhas reais no programa original. Essa abordagem é útil para aperfeiçoar o processo de depuração para programas concorrentes, já que ela diz qual linha deve ser corrigida e quais valores levam a uma execução bem-sucedida. Essa abordagem foi implementada como uma transformação código-a-código de um programa concorrente para um não-determinístico sequencial, o qual é então usado como entrada para ferramentas de verificação existentes. Resultados experimentais mostram que a abordagem descrita é eficaz e é capaz de localizar falhas na maioria dos casos de teste utilizados, extraídos da suíte da International Competition on Software Verification 2015. / Este trabalho descreve uma nova abordagem para localizar falhas em programas concorrentes, a qual é baseada em técnicas de verificação de modelos limitada e sequencialização. A principal novidade dessa abordagem é a ideia de reproduzir um comportamento defeituoso em uma versão sequencial do programa concorrente. De forma a apontar linhas defeituosas, analizam-se os contraexemplos gerados por um verificador de modelos para o programa sequencial instrumentado e procura-se um valor para uma variável de diagnóstico, o qual corresponde a linhas reais no programa original. Essa abordagem é útil para aperfeiçoar o processo de depuração para programas concorrentes, já que ela diz qual linha deve ser corrigida e quais valores levam a uma execução bem-sucedida. Essa abordagem foi implementada como uma transformação código-a-código de um programa concorrente para um não-determinístico sequencial, o qual é então usado como entrada para ferramentas de verificação existentes. Resultados experimentais mostram que a abordagem descrita é eficaz e é capaz de localizar falhas na maioria dos casos de teste utilizados, extraídos da suíte da International Competition on Software Verification 2015.
| Identifer | oai:union.ndltd.org:IBICT/oai:http://localhost:tede/6788 |
| Date | 14 September 2018 |
| Creators | Alves, Erickson Higor da Silva, (92) 992280884 |
| Contributors | eddie_batista@yahoo.com.br, Lima Filho, Eddie Batista de, Cordeiro, Lucas Carvalho |
| 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 | -5930111888266832212, 500 |
Page generated in 0.0019 seconds