Desenvolvimento formal de sistemas críticos: caso de estudo usando SPARK

Abstract

Os métodos formais agregam todo um conjunto de linguagens, tecnologias e ferramentas baseadas em matemática (lógica, teoria de conjuntos) para a especificação, desenvolvimento e validação de sistemas de software. A sua utilização é, em certos domínios, inclusivamente obrigatória para a certificação de componentes de software crítico segundo os níveis mais elevados de segurança.

Neste contexto, pretende-se com este trabalho avaliar em termos práticos e com o uso do SPARK, a utilização dos métodos formais, nomeadamente o paradigma "Correctness by Construction", no desenvolvimento de sistemas críticos. A linguagem SPARK consiste num subconjunto da linguagem Ada, que utiliza anotações (contractos), sob a forma de comentários em Ada, que descrevem o comportamento desejado do componente.

O caso de estudo consiste num microkernel de um sistema operativo de tempo real baseado na arquitectura MILS (Multiple Independent Levels of Security/Safety). A sua modelação procurou cobrir os requisitos de segurança impostos pelos mais elevados níveis de certificação.

Formal methods comprise a wide set of languages, technologies and tools based on mathematics (logic, set theory) for speci cation, development and validation of software systems. In some domains, its use is mandatory for certification of critical software components requiring high assurance levels [1, 2]. In this context, the aim of this work is to evaluate, in practice and using SPARK [3], the usage of formal methods, namely the "Correctness by Construction" paradigm [4], in the development of critical systems. SPARK is a subset of Ada language that uses annotations (contracts), in the form of Ada comments, which describe the desired behavior of the component. Our case study is a microkernel of a real-time operating system based on MILS (Multiple Independent Levels of Security/Safety) architecture [5]. It was formally developed in an attempt to cover the security requirements imposed by the highest levels of certifcation.