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 |
| id |
oai:https:--tede.ufam.edu.br-handle-:tede-4752 |
|---|---|
| recordtype |
dspace |
| spelling |
oai:https:--tede.ufam.edu.br-handle-:tede-47522023-01-31T20:57:14Z Verificação de sistemas de software baseada em transformações de código usando Bounded Model Checking Rocha, Herbert Oliveira Barreto, Raimundo da Silva http://lattes.cnpq.br/2284500318304899 http://lattes.cnpq.br/1132672107627968 Dias Neto, Arilo Claudio http://lattes.cnpq.br/9112415346373126 Lettnin, Djones Vinicius http://lattes.cnpq.br/5048342535708224 Becker, Leandro Buss http://lattes.cnpq.br/4970009027814810 Teste de Software Model Checking Invariantes de Programas Transformações de código CIÊNCIAS EXATAS E DA TERRA: CIÊNCIA DA COMPUTAÇÃO 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. 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. CAPES - Coordenação de Aperfeiçoamento de Pessoal de Nível Superior 2016-01-19T14:54:32Z 2015-07-03 Tese 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. http://tede.ufam.edu.br/handle/tede/4752 por Acesso Aberto application/pdf Universidade Federal do Amazonas Instituto de Computação Brasil UFAM Programa de Pós-graduação em Informática |
| institution |
TEDE - Universidade Federal do Amazonas |
| collection |
TEDE-UFAM |
| language |
por |
| topic |
Teste de Software Model Checking Invariantes de Programas Transformações de código CIÊNCIAS EXATAS E DA TERRA: CIÊNCIA DA COMPUTAÇÃO |
| spellingShingle |
Teste de Software Model Checking Invariantes de Programas Transformações de código CIÊNCIAS EXATAS E DA TERRA: CIÊNCIA DA COMPUTAÇÃO Rocha, Herbert Oliveira Verificação de sistemas de software baseada em transformações de código usando Bounded Model Checking |
| topic_facet |
Teste de Software Model Checking Invariantes de Programas Transformações de código CIÊNCIAS EXATAS E DA TERRA: CIÊNCIA DA COMPUTAÇÃO |
| description |
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. |
| author_additional |
Barreto, Raimundo da Silva |
| author_additionalStr |
Barreto, Raimundo da Silva |
| format |
Tese |
| author |
Rocha, Herbert Oliveira |
| author2 |
http://lattes.cnpq.br/2284500318304899 |
| author2Str |
http://lattes.cnpq.br/2284500318304899 |
| title |
Verificação de sistemas de software baseada em transformações de código usando Bounded Model Checking |
| title_short |
Verificação de sistemas de software baseada em transformações de código usando Bounded Model Checking |
| title_full |
Verificação de sistemas de software baseada em transformações de código usando Bounded Model Checking |
| title_fullStr |
Verificação de sistemas de software baseada em transformações de código usando Bounded Model Checking |
| title_full_unstemmed |
Verificação de sistemas de software baseada em transformações de código usando Bounded Model Checking |
| title_sort |
verificação de sistemas de software baseada em transformações de código usando bounded model checking |
| publisher |
Universidade Federal do Amazonas |
| publishDate |
2016 |
| url |
http://tede.ufam.edu.br/handle/tede/4752 |
| _version_ |
1831969338239746048 |
| score |
11.753896 |