A bounded model checker for SPARK programs

Abstract

Formal verification of software has been an active topic in the area of computer science. Several techniques to verify software are now available, and many tools have been created over the years for different languages and using different techniques. However, for SPARK, a programming language broadly used in critical systems, only deductive verification tools based on contracts are available. The main downside of this approach is the lack of a full automation.

In this dissertation we propose an automated verification tool for SPARK code, thus contributing to fill the gap identified above. Our tool bases on an alternative technique, called bounded model checking, that sacrifices completeness in exchange for automation. Through grounding our work in the highly popular and successful CBMC tool for verification of C code, we investigate how to perform bounded model checking of SPARK programs, and, in particular, we present our implementation of a bounded model checker for SPARK programs called SPARK-BMC.

Experiments performed with our tool show that automatic verification of SPARK programs is feasible and useful, even though is not complete. As far as we know, there is no tool based on such an automated technique for SPARK. The tool is freely available and based on open-source technologies.

A verificação formal de software tem sido um tópico bastante ativo na área das ciências da computação. Várias técnicas podem ser aplicadas para verificar software e ao longo dos anos surgiram várias ferramentas para diferentes linguagens usando diferentes técnicas. Para a linguagem de programação SPARK, que é especialmente usada em sistemas críticos, existem ferramentas dedutivas baseadas em contratos. Porém, esta técnica de verificação tem uma desvantagem: fraca automação. Nesta dissertação, propomos uma ferramenta de verificação automática para código SPARK, assim contribuindo para suprir a limitação antes referida. Esta ferramenta baseia-se numa técnica alternativa denominada por ‘bounded model checking’ que embora não sendo completa permite automação. Baseando o nosso trabalho na popular e bem sucedida ferramenta CBMC para a verificação de código C, estudamos como levar a cabo o ‘bounded model checking’ de programas SPARK e, em particular apresentamos a respectiva implementação que designamos por SPARK-BMC. As experiências que levamos a cabo com a nossa ferramenta mostram que a verificação automática de programas SPARK, ainda que não seja completa, é praticável e útil. Pelo que nos é dado a conhecer, não há nenhuma ferramenta baseada numa tal técnica automatizada para programas SPARK. A ferramenta é de acesso livre e baseia-se em tecnologias ‘open-source’.