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

• Main Author: Rocha, Herbert Oliveira
• Other Authors: Barreto, Raimundo da Silva
• Format: Others
• Language: Portuguese
• Published: Universidade Federal do Amazonas 2016
• Subjects: Teste de Software; Model Checking; Invariantes de Programas; Transformações de código; CIÊNCIAS EXATAS E DA TERRA: CIÊNCIA DA COMPUTAÇÃO
• Online Access: http://tede.ufam.edu.br/handle/tede/4752

Submitted by Lúcia Brandão ([e-mail]) on 2015-12-11T18:49:43Z No. of bitstreams: 1 Tese - Herbert Oliveira Rocha.pdf: 2090300 bytes, checksum: 94ec40933733aec0a76afd0916b0f8cb (MD5) === Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central ([e-mail]) on 2016-01-19T14:41:05Z (GMT) No. of bitstreams: 1 Tese - Herbert Oliveira Rocha.pdf: 2090300 bytes, checksum: 94ec40933733aec0a76afd0916b0f8cb (MD5) === Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central ([e-mail]) on 2016-01-19T14:54:32Z (GMT) No. of bitstreams: 1 Tese - Herbert Oliveira Rocha.pdf: 2090300 bytes, checksum: 94ec40933733aec0a76afd0916b0f8cb (MD5) === Made available in DSpace on 2016-01-19T14:54:32Z (GMT). No. of bitstreams: 1 Tese - Herbert Oliveira Rocha.pdf: 2090300 bytes, checksum: 94ec40933733aec0a76afd0916b0f8cb (MD5) Previous issue date: 2015-07-03 === CAPES - Coordenação de Aperfeiçoamento de Pessoal de Nível Superior === Oneofthemainchallenges insoftwaredevelopment istoensurethesafetyofthesoftwaresystems, especially in critical embedded systems, such as aircraft or healthcare, where several constraints (e.g., response time and data accuracy) must be met and measured in accordance with the user requirements, otherwise a failure can lead to catastrophic situations. Thus, software verification and testing techniques are essential items for the software development with quality, where such techniques aim to confirm the user requirements, as well as, the predetermined behaviors for the software. In the software verification context, aiming the product quality, the formal verification technique called model checking has been used to find subtle errors in actual projects of the software systems. However, the use of the model checking technique presents some challenges such as dealing with the model’s state explosion problem, integration with software testing environments more familiar to designers, and handling counter-examples to reproduce the identified errors. In order to deal with these problems, a possible solution is to explore the characteristics already provided by the model checkers, e.g., verification of the safety properties and generation of counter-examples. Exploring this set of characteristics, coupled with the use of program invariants inference and a special kind of model checking, called Bounded Model Checking (BMC), this thesis presents a set of methods to complement and enhance the scalability and accuracy of the verification performed by Bounded Model Checkers. These methods adopted code transformation techniques to explore the characteristics of Bounded Model Checkers to analyze the safety properties and demonstrate errors in programs written inthe C programming language. The methods presented in this thesis are: (1) The automatic generation and verification of the test cases based on safety properties generated by a Bounded Model Checker for unit tests; (2) Automating thecollection andmanipulation of thedatafrom thecounter-examples, todemonstrate the main cause of the identified error; and (3) Adopting program invariants dynamically/statically inferred from the analyzed program, to restrict the exploration of the states sets while performing the verification by the BMC. This way, helping to improve the verification performed by a BMC, related to assist in the verification and accuracy of results, by adoption of the program invariants. The proposed approaches when used separately, provide additional options to the verification, and interconnected, improving the code verification. Theexperimental results of theproposed methods show to be efficient over public available benchmarks of C programs, finding errors not previously found byother methods that are state-of-the-art. === 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.