Formal verification of Ada programs: an approach based on model checking

Abstract

O rápido crescimento da complexidade dos sistemas de software exige, agora mais do que nunca, uma validação rigorosa dos mesmos por forma a manter ou até mesmo aumentar a confiança nestes sistemas. Em particular nos sistemas críticos, onde as falhas podem ter consequências catastróficas podendo até incluir a perca de várias vidas humanas, é de externa importância o desenvolvimento de técnicas capazes de garantir altos níveis de confiança para estes sistemas. Nesta tese é proposta a utilização de uma técnica formal para a verificação de programas Ada, que pretende aumentar a confiança em sistemas cuja implementação seja realizada nesta linguagem de programação. Mais precisamente, pretende-se a aplicação da técnica de verificação de modelos para a análise do código fonte de programas concorrentes Ada, com especial foco para o domínio dos sistemas críticos. A verificação de modelos é uma técnica bem-sucedida no que diz respeito à garantia de um aumento de fiabilidade destes sistemas. No entanto, a aplicação desta técnica a sistemas de software enfrenta ainda vários obstáculos, e as ferramentas e técnicas para ajudar a ultrapassar estes obstáculos estão ainda a ser desenvolvidas. A ferramenta desenvolvida no contexto desta tese (ATOS) visa responder a problemas como (i) a construção de modelos a partir de programas e (ii) a especificação de propriedades para estes modelos de acordo com as pretendidas para os programas. A construção manual de modelos que simulam o comportamento de programas é um processo complexo, temporalmente dispendioso, e sujeito a falhas devido à complexidade destes sistemas. De forma a ultrapassar este problema o ATOS propõe a extração automática de modelos a partir de programas Ada. Por outro lado, o mapeamento das propriedades desejadas dos programas em propriedades dos modelos pode ser urna tarefa com um grau de complexidade elevado, pois requer entre outros a utilização de um formalismo logico ao qual a maioria dos programadores não está acostumada. 0 ATOS ajuda no mapeamento destas propriedades, oferecendo vários mecanismos de suporte à sua especificação.

The rapid growth of the complexity of software systems demands, flow more than ever, a rigorous validation of these systems in order to maintain or even increase their reliability. In particular in high-integrity systems, where failures may have catastrophic consequences which may even include the lost of human lives, the development of verification techniques capable of ensuring high degrees of confidence is seen as extremely important. In this thesis the use of a formal technique for the verification of Ada programs is proposed, which aims to increase the reliability of systems whose implementation is based on this programming language. More precisely, we target the application of the model checking technique to the verification of source code of concurrent Ada programs, with a special focus on the critical systems domain. Model checking is a well-succeeded technique for providing increased levels of assurance regarding system correctness. However, its application to software systems still faces several obstacles, and the necessary tools and techniques to help in the overcoming of these problems are still being developed. The tool presented in this thesis (ATOS) addresses the problems of (i) constructing models from programs and (ii) specifying properties for models corresponding to the ones desired for programs. The manual construction of models that simulate the behavior of programs is a time-costly, complex and error-prone process, due to the complexity of these systems. In order to overcome this problem, ATOS proposes the automatic extraction of models from Ada programs. On the other hand, the mapping of the desired properties from programs to models can be a task of high complexity, because it requires among others that they are expressed in a logical formalism that most programmers are not acquainted with. ATOS helps in this mapping task by providing several mechanisms aiming to support the specification of properties.