Spelling suggestions: "subject:"verificação dde 5oftware"" "subject:"verificação dde 1software""
1 |
Verificação de Programas Embarcados ANSI-C baseada em indução Matemática e InvariantesMelo, Raimundo Williame Rocha de, 92-99345-3625 10 August 2017 (has links)
Submitted by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2018-03-21T17:40:38Z
No. of bitstreams: 2
license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5)
Dissertação_Raimundo W. R. Melo.pdf: 1511352 bytes, checksum: 35f1429da9fc237f23a6e983f4c6abd9 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2018-03-21T17:40:50Z (GMT) No. of bitstreams: 2
license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5)
Dissertação_Raimundo W. R. Melo.pdf: 1511352 bytes, checksum: 35f1429da9fc237f23a6e983f4c6abd9 (MD5) / Made available in DSpace on 2018-03-21T17:40:50Z (GMT). No. of bitstreams: 2
license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5)
Dissertação_Raimundo W. R. Melo.pdf: 1511352 bytes, checksum: 35f1429da9fc237f23a6e983f4c6abd9 (MD5)
Previous issue date: 2017-08-10 / FAPEAM - Fundação de Amparo à Pesquisa do Estado do Amazonas / 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. / 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.
|
2 |
Proposta de metodologia para utilização em hardware reconfigurável para aplicações aeroespaciais / Proposal methodology for use in reprogrammable hardware in aerospace applicationsCastellar, Anderson 19 September 2008 (has links)
O programa CBERS é uma parceria entre o governo Brasileiro e o governo Chinês para desenvolvimento de satélites para sensoriamento remoto. A metodologia proposta será aplicada na Câmera Multi Espectral (MUXCAM) dos satélites CBERS-3 e 4, a primeira deste gênero a ser totalmente produzida no Brasil. Devido à alta confiabilidade exigida, principalmente devido ao custo elevado, as aplicações aeroespaciais que envolvem hardware reconfigurável devem possuir uma metodologia de desenvolvimento, desde a definição dos requisitos até o processo de verificação e validação. A utilização da linguagem VHDL e da ferramenta de síntese, processo este chamado de metodologia clássica, produzem um circuito final não otimizado, eliminando redundâncias e alterando a arquitetura proposta. Este trabalho propõe uma metodologia que busca garantir a utilização de uma única arquitetura desde o início do ciclo de desenvolvimento até sua finalização. Esta metodologia torna o processo de desenvolvimento mais confiável e determinístico. / The CBERS program is a partnership between Brazil and China to produce satellites for remote sensing, producing images of the Earth for studies in several areas, mainly the ones related to the sustainable exploitation of natural resourses. The methodology proposed in this work will be applied on the satellite CBERS-3 e 4\'s Multispectral Camera (MUXCAM), the first of its gender fully produced in Brazil. Because the high reliability involved in aerospace applications, a methodology is necessary from software specification until the verification and validation process to guarantee the high reliability. The use of the synthesis tool and VHDL produce a poor circuit, eliminating redundance and making architectural changes. This work proposes a methodology to keep the architectural the same all development cycle, make the development process more trustful for aerospace applications.
|
3 |
Proposta de metodologia para utilização em hardware reconfigurável para aplicações aeroespaciais / Proposal methodology for use in reprogrammable hardware in aerospace applicationsAnderson Castellar 19 September 2008 (has links)
O programa CBERS é uma parceria entre o governo Brasileiro e o governo Chinês para desenvolvimento de satélites para sensoriamento remoto. A metodologia proposta será aplicada na Câmera Multi Espectral (MUXCAM) dos satélites CBERS-3 e 4, a primeira deste gênero a ser totalmente produzida no Brasil. Devido à alta confiabilidade exigida, principalmente devido ao custo elevado, as aplicações aeroespaciais que envolvem hardware reconfigurável devem possuir uma metodologia de desenvolvimento, desde a definição dos requisitos até o processo de verificação e validação. A utilização da linguagem VHDL e da ferramenta de síntese, processo este chamado de metodologia clássica, produzem um circuito final não otimizado, eliminando redundâncias e alterando a arquitetura proposta. Este trabalho propõe uma metodologia que busca garantir a utilização de uma única arquitetura desde o início do ciclo de desenvolvimento até sua finalização. Esta metodologia torna o processo de desenvolvimento mais confiável e determinístico. / The CBERS program is a partnership between Brazil and China to produce satellites for remote sensing, producing images of the Earth for studies in several areas, mainly the ones related to the sustainable exploitation of natural resourses. The methodology proposed in this work will be applied on the satellite CBERS-3 e 4\'s Multispectral Camera (MUXCAM), the first of its gender fully produced in Brazil. Because the high reliability involved in aerospace applications, a methodology is necessary from software specification until the verification and validation process to guarantee the high reliability. The use of the synthesis tool and VHDL produce a poor circuit, eliminating redundance and making architectural changes. This work proposes a methodology to keep the architectural the same all development cycle, make the development process more trustful for aerospace applications.
|
Page generated in 0.0876 seconds