Verificação e comprovação de erros em códigos C usando bounded model checker

• Ano de defesa: 2011
• Autor(a) principal: Rocha, Herbert Oliveira
• Outros Autores: http://lattes.cnpq.br/2284500318304899
• Tipo de documento: Dissertação
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: Universidade Federal do Amazonas; Instituto de Computação; BR; UFAM; Programa de Pós-graduação em Informática
• Palavras-chave em Português: Model checking; Bounded model checker; Propriedades de segurança; Contra-exemplos; Comprovação de Erros; Bounded modelchecker; Safety properties; Counterexamples; Proving errors; CIÊNCIAS EXATAS E DA TERRA: CIÊNCIA DA COMPUTAÇÃO
• Link de acesso: http://tede.ufam.edu.br/handle/tede/2965

A utilização de sistemas baseados em computador em diversos domínios aumentou significativamente nos últimos anos. Um dos principais desafios no desenvolvimento de software de sistemas críticos é a garantia da sua correção e confiabilidade. Desta forma, a verificação de software exerce um papel importante para assegurar a qualidade geral do produto, visando principalmente características como previsibilidade e confiabilidade. No contexto de verificação de software, os Bounded Model Checkers estão sendo utilizados para descobrir erros sutis em projetos de sistemas de software atuais, contribuindo eficazmente neste processo de verificação. O valor dos contra-exemplos e propriedades de segurança gerados pelo Bounded Model Checkers para criar casos de testes e para a depuração de sistemas é amplamente reconhecido. Quando um Bounded Model Checking (BMC) encontra um erro ele produz um contra-exemplo. Assim, o valor dos contra-exemplos para depuração de software é amplamente reconhecido no estado da prática. Entretanto, os BMCs frequentemente produzem contra-exemplos que são grandes ou difíceis de entender ou manipular, principalmente devido ao tamanho do software e valores escolhidos pelo solucionador de satisfabilidade. Neste trabalho visamos demonstrar e analisar o uso de método formal (através da técnica model checking) no processo de desenvolvimento de programas na linguagem C, explorando as características já providas pelo model checking como o contra-exemplo e a identificação e verificação de propriedades de segurança. Em face disto apresentamos duas abordagens: (i) descrevemos um método para integrar o Bounded Model Checker ESBMC como o framework de teste unitário CUnit, este método visa extrair as propriedades geradas pelo ESBMC para gerar automaticamente casos de teste usando o rico conjunto de assertivas providas pelo framework CUnit e (ii) um método que visa automatizar a coleta e manipulação dos contra-exemplos, de modo a instanciar o programa C analisado, para comprovar a causa raiz do erro identificado. Tais métodos podem ser vistos como um método complementar para a verificação efetuada pelos BMCs. Demonstramos a eficácia dos métodos propostos sobre benchmarks públicos de código C.