Application of Formal Methods in the ITASAT Project

Abstract

Critical software can be potentially dangerous if not well verified, leading to serious failures. Accordingly, there is a need for improved validation and verification methods in order to have guarantees about the software final product. The aim of this project is to define a more linear and organized verification and validation plan to, formally, verify the most critical parts of the OBDH (On-Board Data Handling) subsystem of ITASAT, supported by the Alloy formal language.

Alloy supports the description of systems whose state involves complex relational structure. The application of Alloy and Alloy Analyzer was motivated by the need for a formal specification that is more closely tailored to state-machines, and more amenable to automatic analysis. Structural and behavioural properties are described declaratively, by conjoining relations and constrains, making it possible to develop and analyze a model incrementally. Due to the high cost of using these methods, they are mainly used in the development of high-critical software where safety and security are crucial.

This dissertation presents a set of guidelines for analysis and modelling of software systems which support the creation of a formal model and allow some extra behaviours such as synchronization, interruptions and flags. A new tool, ModelMaker, was developed in order to create models using these guidelines in a more interactive way.

O software crítico torna-se potencialmente perigoso quando não cuidadosamente verificado, podendo resultar em falhas graves. Por consequência, existe uma necessidade de melhorar os métodos de validação e verificação, oferecendo garantias sobre o produto final. O objetivo do presente projeto e a definição de um plano de verificação e validação linear e organizado para verificar formalmente as partes mais críticas do subsistema OBDH (On- Board Data Handling) do Satélite do ITA (Instituto de Tecnologia Aeronáutica), através da linguagem formal Alloy. Alloy permite a descrição de sistemas cujo estado envolve estruturas relacionais complexas. A sua aplicação e a do Alloy Analyzer justificou-se pela necessidade de uma especificação formal que fosse mais adaptada a máquinas de estado e mais recetiva a análises automáticas. As características estruturais e comportamentais sao descritas declarativamente, através da juncão de relações e restrições, permitindo desenvolver e analisar um modelo de forma iterativa. Devido ao seu custo elevado, estes métodos são principalmente usados no desenvolvimento de softwares críticos, para os quais a segurança e um pressuposto fundamental. Esta dissertação apresenta um conjunto de diretrizes para a análise e modelação de sistemas. Estas suportam a criação de um modelo formal e permitem alguns comportamentos adicionais como a sincronização, a interrupção e ags. E também introduzido o ModelMaker, uma ferramenta que, fazendo uso das directrizes, ajuda numa construção interativa e automática de modelos.