Verificação de sistemas de software baseada em transformações de código usando Bounded Model Checking

• Ano de defesa: 2015
• Autor(a) principal: Rocha, Herbert Oliveira
• Outros Autores: http://lattes.cnpq.br/2284500318304899
• Tipo de documento: Tese
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: Universidade Federal do Amazonas; Instituto de Computação; Brasil; UFAM; Programa de Pós-graduação em Informática
• Palavras-chave em Português: Teste de Software; Model Checking; Invariantes de Programas; Transformações de código; CIÊNCIAS EXATAS E DA TERRA: CIÊNCIA DA COMPUTAÇÃO
• Link de acesso: http://tede.ufam.edu.br/handle/tede/4752

Um dos principais desafios no desenvolvimento de software é garantir a funcionalidade dos sistemas de software, especialmente em sistemas embarcados críticos, tais como aeronáutico ou hospitalar, onde diversas restrições (por exemplo, tempo de resposta e precisão dos dados) devem ser atendidas e mensuradas de acordo com os requisitos do usuário, caso contrário uma falha pode conduzir a situações catastróficas. Logo, técnicas de verificação e teste de software são itens indispensáveis para um desenvolvimento com qualidade, onde tais técnicas visam confirmar os requisitos do usuário, bem como os comportamentos pré-estabelecidos para osoftware. No contexto de verificação de software, visando à qualidade geral do produto, a técnica de verificação formal model checking tem sido utilizada para descobrir erros sutis em projetos de sistemas de software atuais. Contudo, a utilização da técnica model checking apresenta alguns desafios, tais como, lidar com a explosão do espaço de estados do modelo, integração com outros ambientes de testes mais familiares aos projetistas e tratamento e análise de contra-exemplos para reprodução de erros. De modo a lidar com estes problemas, uma possível solução é explorar as características já providas pelos model checkers, por exemplo, a verificação de propriedades de segurança e geração de contra-exemplos. Explorando este conjunto de características, juntamente com autilização dainferência deinvariantes eumtipo especial demodelchecking, denominado de BoundedModelChecking (BMC),esta tese apresenta um conjunto de métodos para complementar e aprimorar a escalabilidade e acurácia da verificação efetuada por Bounded Model Checkers. Estes métodos utilizam técnicas de transformações de código para explorar as características de Bounded Model Checkers, a fim de analisar propriedades de segurança e demonstrar erros em códigos escritos na linguagem de programação C. Os métodos apresentados nesta tese são: (1) A geração e verificação automática de casos de teste baseado em propriedades de segurança geradas por um Bounded Model Checker para testes de unidade; (2) Automatizar acoleta emanipulação das informações dos contra-exemplos, de modo a demonstrar a causa principal do erro identificado; e (3) Utilização de invariantes dinamicamente/estaticamente inferidas, a partir do programa analisado, para restringir a exploração dos conjuntos de estados durante a execução da verificação pelo BMC. Desta forma, ajudando no aprimoramento da verificação efetuada por um BMC, no que concerne em auxiliar a sua verificação e na precisão dos resultados, pela utilização de invariantes de programas. As abordagens propostas, quando utilizadas isoladamente, fornecem alternativas complementares a verificação e, interligadas, aprimoram a verificação de código. Os resultados experimentais dos métodos propostos demonstram ser eficientes sobre benchmarks públicos de programas em C, encontrando defeitos não anteriormente encontrados por outros métodos que são estado-da-arte.