/img alt="Imagem da capa" class="recordcover" src="""/>
Tese
Verificação de sistemas de software baseada em transformações de código usando Bounded Model Checking
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 m...
Autor principal: | Rocha, Herbert Oliveira |
---|---|
Outros Autores: | http://lattes.cnpq.br/2284500318304899 |
Grau: | Tese |
Idioma: | por |
Publicado em: |
Universidade Federal do Amazonas
2016
|
Assuntos: | |
Acesso em linha: |
http://tede.ufam.edu.br/handle/tede/4752 |
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. |