| Name: | Description: | Size: | Format: | |
|---|---|---|---|---|
| 3.34 MB | Adobe PDF |
Advisor(s)
Abstract(s)
A verificação formal de software é uma área da Ciência de Computadores com grande importância no desenvolvimento de projetos de alta integridade. Ao adotar a verificação formal como uma das componentes dos projetos de software, aumenta-se a compreensão da natureza e propósito do programa por parte do programador e faz com que este se foque na precisão e consistência. Por outro lado, obriga também o programador a optar por soluções mais simples e que respeitem os requisitos de implementação, pois quanto mais complexo for o código desenvolvido maior será o esforço de prova e a dificuldade da mesma ser obtida de forma automática. Uma consequência é a minimização do risco de introdução de erros e maior facilidade na manutenção do programa.
A linguagem SPARK e o seu conjunto de ferramentas favorecem o desenvolvimento de programas da forma que é descrita no parágrafo anterior. Face às características da linguagem que impõe restrições, muitos erros de programação que são comuns noutras linguagens não acontecem.
O objetivo desta dissertação é o de estudar a usabilidade do SPARK2014 na implementação de estruturas de dados e algoritmos simples que são tipicamente utilizados no desenvolvimento de sistemas críticos ou de elevada integridade. Serão desenvolvidas especificações formais para os algoritmos em estudo, bem como implementações destes que são consistentes com essas mesmas especificações.
Por fim será feita uma análise a todo o processo, no sentido de obter indicadores do real valor do SPARK2014 no desenvolvimento de aplicações mais complexas.
Formal verification of software is an area of Computer Science with increasing importance and especially relevant for high-integrity projects. By adopting formal verification, programmers are brought to know better the nature of the algorithms they are implementing which need to be accurate and consistent. These properties are usually not simple to verify and as result of such complexity programmers tend to choose simpler solutions to minimize verification costs. Simple solutions have clear advantages in terms of error detection and maintenance. The Spark language and its toolset have become a popular solution among high-integrity software production industry since it helps to produce correct software. The new Spark 2014 is a completely new version of the tool with a completely new approach to the verification process. The aim of this work is to study the usability of the new SPARK 2014 in implementing data structures and algorithms commonly used in the development of high integrity systems and understand the real advantages of the trade-off imposed by a new, more complex approach. This goal is achieved by developing specification and implementing a set of selected algorithms using Spark 2014.
Formal verification of software is an area of Computer Science with increasing importance and especially relevant for high-integrity projects. By adopting formal verification, programmers are brought to know better the nature of the algorithms they are implementing which need to be accurate and consistent. These properties are usually not simple to verify and as result of such complexity programmers tend to choose simpler solutions to minimize verification costs. Simple solutions have clear advantages in terms of error detection and maintenance. The Spark language and its toolset have become a popular solution among high-integrity software production industry since it helps to produce correct software. The new Spark 2014 is a completely new version of the tool with a completely new approach to the verification process. The aim of this work is to study the usability of the new SPARK 2014 in implementing data structures and algorithms commonly used in the development of high integrity systems and understand the real advantages of the trade-off imposed by a new, more complex approach. This goal is achieved by developing specification and implementing a set of selected algorithms using Spark 2014.
Description
Keywords
Verificação formal VCs SPARK Alta integridade Why3 Formal Verification High Integrity Systems