Exportar este item: EndNote BibTex

Use este identificador para citar ou linkar para este item: https://tede.ufam.edu.br/handle/tede/6261
Tipo do documento: Dissertação
Título: Verificação de Programas Embarcados ANSI-C baseada em indução Matemática e Invariantes
Autor: Melo, Raimundo Williame Rocha de 
Primeiro orientador: Cordeiro, Lucas Carvalho
Primeiro coorientador: Lima Filho, Eddie Batista de
Primeiro membro da banca: Barreto, Raimundo da Silva
Segundo membro da banca: Rocha, Herbert Oliverira
Resumo: O uso de sistemas embarcados, sistemas computacionais especializados para execução em sistemas eletrônicos ou mecânicos tem crescido de forma vertiginosa devido a utilização cada vez mais intensa de sensores, interfaces de rede e protocolos de comunicação em diversas áreas. Por isso, é cada vez mais importante garantir a robustez desses sistemas, uma vez que estão se tornando mais complexos e integrados. Existem várias técnicas para garantir que um sistema seja entregue ao cliente sem erros, em particular, a verificação formal dos programas tem se revelado eficaz na busca de falhas. Neste trabalho é descrito um algoritmo de indução matemática conhecido como k-induction combinado ao uso de invariantes para verificar e refutar propriedades de segurança em programas desenvolvidos na linguagem ANSI-C. Em particular, a abordagem proposta infere invariantes no programa para auxiliar na verificação de programas ANSI-C através da técnica de indução matemática através do refinamento de restrição (i.e, poliédrico) para especificar pré- e pós-condições. No método proposto, adotamos dois geradores de invariantes para produzir e alimentar o algoritmo de indução matemática o qual é implementado na ferramenta Efficient SMT-Based Context-Bounded Model Checker. A motivação para a combinação de invariantes com o algoritmo de indução matemática é fechar um gap na verificação formal de programas que possuam variáveis globais, além de programas com loops que possuem desvios condicionais e o número de iterações é desconhecido. PIPS e PAGAI são as ferramentas utilizadas para analisar o código e produzir invariantes indutivas responsáveis por guiar o algoritmo de indução matemática na verificação do benchmark, sendo este o principal desafio do método proposto. Para avaliar a eficácia da abordagem proposta neste trabalho, além de aplicações de Sistemas Embarcados foram utilizados benchmarks públicos disponibilizados pela Competição Internacional de Verificação de Software onde participam Universidades, pesquisadores, estudandantes de doutorado de várias partes do mundo, e fornece amplo conjunto de casos de teste para verificação. Além disso, foram utilizadas ferramentas estado-da-arte para a comparação dos resultados e, assim mensurar a eficácia do método proposto. Os resultados experimentais foram positivos e mostraram que o algoritmo de indução matemática com invariantes pode verificar uma grande variedade de propriedades de segurança em programas com loops e aplicações de sistemas embarcados de telecomunicações, sistemas de controle e dispositivos médicos.
Abstract: The use of embedded systems, i.e., computer systems focused on performing specific functions in larger (electronic or mechanical) systems, has been growing lately, and ensuring the robustness of such systems has become increasingly important. There are several techniques to ensure that a system is released without errors. In particular, formal verification of programs is proving itself to be effective in the search for failures. In this work, an induction-proof algorithm is described, which combines k-induction and invariants to verify and refute safety properties in embedded ANSI-C software. Moreover, the proposed k-induction-based approach infers invariants in the program to assist in verification tasks, using constraint refinement (i.e., polyhedral) to specify pre- and post-conditions. We adopted two invariant generators to produce such and feed the k-induction algorithm, which is implemented in the Efficient SMT-Based Context-Bounded Model Checker tool. Public benchmarks were used to assess the effectiveness of our approach. In addition, a comparison to other state-of-the-art verification tools using a set of benchmarks from the International Competition for Software Verification in addition to embedded systems applications. Experimental results have shown that the proposed approach, with and without invariants, can verify a wide variety of safety properties in programs with loops and embedded software from telecommunications, control systems, and medical domains.
Palavras-chave: Verificação formal
Indução matemática
Invariantes indutivas
PIPS
PAGAI
Verificação de Software
Sistemas embarcados
Área(s) do CNPq: ENGENHARIAS: ENGENHARIA ELÉTRICA
Idioma: por
País: Brasil
Instituição: Universidade Federal do Amazonas
Sigla da instituição: UFAM
Departamento: Faculdade de Tecnologia
Programa: Programa de Pós-graduação em Engenharia Elétrica
Citação: MELO, Raimundo Williame Rocha de. Verificação de Programas Embarcados ANSI-C baseada em indução Matemática e Invariantes. 2017. 70 f. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas, Manaus, 2017.
Tipo de acesso: Acesso Aberto
Endereço da licença: http://creativecommons.org/licenses/by-nc-nd/4.0/
URI: https://tede.ufam.edu.br/handle/tede/6261
Data de defesa: 10-Ago-2017
Aparece nas coleções:Mestrado em Engenharia Elétrica

Arquivos associados a este item:
Arquivo Descrição TamanhoFormato 
Dissertação_Raimundo W. R. Melo.pdf1,48 MBAdobe PDFThumbnail

Baixar/Abrir Pré-Visualizar


Este item está licenciada sob uma Licença Creative Commons Creative Commons