Exportar este item: EndNote BibTex

Use este identificador para citar ou linkar para este item: https://tede.ufam.edu.br/handle/tede/4752
Tipo do documento: Tese
Título: Verificação de sistemas de software baseada em transformações de código usando Bounded Model Checking
Autor: Rocha, Herbert Oliveira 
Primeiro orientador: Barreto, Raimundo da Silva
Primeiro coorientador: Cordeiro, Lucas Carvalho
Primeiro membro da banca: Dias Neto, Arilo Claudio
Segundo membro da banca: Lettnin, Djones Vinicius
Terceiro membro da banca: Becker, Leandro Buss
Resumo: 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.
Abstract: 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.
Palavras-chave: Teste de Software
Model Checking
Invariantes de Programas
Transformações de código
Área(s) do CNPq: CIÊNCIAS EXATAS E DA TERRA: CIÊNCIA DA COMPUTAÇÃO
Idioma: por
País: Brasil
Instituição: Universidade Federal do Amazonas
Sigla da instituição: UFAM
Departamento: Instituto de Computação
Programa: Programa de Pós-graduação em Informática
Citação: ROCHA, Herbert Oliveira. Verificação de sistemas de software baseada em transformações de código usando Bounded Model Checking. 2015. 158 f. Tese (Doutorado em Informática) - Universidade Federal do Amazonas, Manaus, 2015.
Tipo de acesso: Acesso Aberto
URI: http://tede.ufam.edu.br/handle/tede/4752
Data de defesa: 3-Jul-2015
Aparece nas coleções:Mestrado em Informática

Arquivos associados a este item:
Arquivo Descrição TamanhoFormato 
Tese - Herbert Oliveira Rocha.pdfTese - Herbert Oliveira Rocha2,04 MBAdobe PDFThumbnail

Baixar/Abrir Pré-Visualizar


Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.