| Name: | Description: | Size: | Format: | |
|---|---|---|---|---|
| 1.12 MB | Adobe PDF |
Authors
Advisor(s)
Abstract(s)
This research work is in the scope of the Master course in Computer Science of University of
Beira Interior dissertation and introduces the research undertaken in a Master Thesis done in
collaboration with Critical Software, SA.
This document presents the effort for verification and validation of ExoMars Trace Gas Orbiter
Central Software that was fully implemented by Critical Software in cooperation with Thales
Alenia Space, for an European Space Agency exploration of Mars atmosphere mission. The work
was an Ada implemented code reformulation to SPARK aiming the capability evaluation of code
analysis and Design-by-Contract techniques for validation and verification of a spacecraft on
board software.
On Safety Mission-Critical systems the importance of secure and reliable software path to the
introduction of new high integrity development methods as an efficient and low cost alternative
of software testing. As Edger Dijsktra said, testing software only detect the presence of bugs
but not prove his absence and, besides that, it is a late detection. There is an increased need
of safety and functional properties assurance before the system deployment.
Design-by-Contract approach is a kind of formal code verification, based on Hoare Logic, that
can reduce the costs in two ways, because it gave earlier high guarantees that code is free of runtime
errors and run as expected, in the development phase where bugs correction is cheaper.
SPARK toolset is used to perform formal code verification for Ada programming language, mostly
used on Safety Mission-Critical systems development. SPARK analysis is targeted for assurance
of correct information flow and the correct behaviour of programs execution.
Este trabalho de investigação está inserido no âmbito da dissertação do curso de Mestrado em Engenharia Informática da Universidade da Beira Interior realizado em contexto industrial na empresa Critical Software, SA. Este documento apresenta o projeto de verificação e validação formal do Software Central do ExoMars Trace Gas Orbiter que foi totalmente implementado pela Critical Software em parceria com a Thales Alenia Space, para uma missão da Agência Espacial Europeia direcionada à exploração da atmosfera Marciana. O trabalho realizado tratou da reformulação do código implementado em Ada para SPARK com o objetivo de avaliar as suas capacidades de análise de código e as técnicas de Design-by-Contract para validação e verificação formal do software de voo de um satélite. Em sistemas Safety Mission-Critical a importância de um software seguro e confiável conduz à introdução novos métodos de desenvolvimento com grande integridade como uma alternativa aos testes de software eficiente e de baixo custo. Tal como Edger Dijsktra disse, testar software apenas deteta a presença de erros mas não prova a sua ausência e, para além disso, a deteção é tardia. Existe uma cresente necessidade de assegurar as propriedades funcionais e de safety do sistema na fase de pré-produção. A abordagem Design-by-Contract é um tipo de verificação formal de código, baseada na Lógica de Hoare, que pode reduzir os custos de duas formas, porque dá-nos elevadas garantias de que o código está livre de erros de execução e que irá executar como pretendido, logo na fase de desenvolvimento onde a correção de erros é menos custosa. A ferramenta SPARK é usada para realizar a verificação formal de código para a linguagem de programação Ada, usado na maioria dos casos para o desenvolvimento de sistemas Safety Mission-Critical. A análise do SPARK é direcionada para a garantia de um correto fluxo de informação e o correto comportamente na execução dos programas.
Este trabalho de investigação está inserido no âmbito da dissertação do curso de Mestrado em Engenharia Informática da Universidade da Beira Interior realizado em contexto industrial na empresa Critical Software, SA. Este documento apresenta o projeto de verificação e validação formal do Software Central do ExoMars Trace Gas Orbiter que foi totalmente implementado pela Critical Software em parceria com a Thales Alenia Space, para uma missão da Agência Espacial Europeia direcionada à exploração da atmosfera Marciana. O trabalho realizado tratou da reformulação do código implementado em Ada para SPARK com o objetivo de avaliar as suas capacidades de análise de código e as técnicas de Design-by-Contract para validação e verificação formal do software de voo de um satélite. Em sistemas Safety Mission-Critical a importância de um software seguro e confiável conduz à introdução novos métodos de desenvolvimento com grande integridade como uma alternativa aos testes de software eficiente e de baixo custo. Tal como Edger Dijsktra disse, testar software apenas deteta a presença de erros mas não prova a sua ausência e, para além disso, a deteção é tardia. Existe uma cresente necessidade de assegurar as propriedades funcionais e de safety do sistema na fase de pré-produção. A abordagem Design-by-Contract é um tipo de verificação formal de código, baseada na Lógica de Hoare, que pode reduzir os custos de duas formas, porque dá-nos elevadas garantias de que o código está livre de erros de execução e que irá executar como pretendido, logo na fase de desenvolvimento onde a correção de erros é menos custosa. A ferramenta SPARK é usada para realizar a verificação formal de código para a linguagem de programação Ada, usado na maioria dos casos para o desenvolvimento de sistemas Safety Mission-Critical. A análise do SPARK é direcionada para a garantia de um correto fluxo de informação e o correto comportamente na execução dos programas.
Description
Keywords
Análise de Fluxo Design-By-Contract Exomars Métodos Formais Sistemas Safety Mission-Critical Verificação Formal de Código