Dissertação

On the Application of Model Checking Techniques to Real-Time Hypervisors in the Context of Integrated Modular Avionics Systems EVALUATED

O carácter crítico, em termos de segurança, da maioria dos sistemas aviónicos, tais como aeronaves e naves espaciais, requer uma análise cuidadosa da sua correção antes destes serem lançados para uso. Para este fim, técnicas mais robustas do que testes devem ser utilizadas para o estudo da correção dos mesmos. Deste modo, métodos formais, em particular verificação de modelos, uma técnica de verificação automática para sistemas concorrentes com um número de estados finito, surgem como uma solução alternativa para a verificação de propriedades de sistemas. O objetivo do nosso trabalho é utilizar sistemas de verificação formal, nomeadamente o Spin e TLC, para verificar partes do hipervisor em tempo-real desenvolvido pela GMV. Durante a dissertação, iremos modelar e examinar, recorrendo aos sistemas anteriores, problemas de concorrência específicos do sistema distribuído em tempo-real que constitui o nosso caso de estudo, nomeadamente particionamento de tempo, comunicação entre processos através de memória partilhada e modelos de memória. O nosso maior contributo corresponde à descoberta de um erro de implementação, que causava processos concorrentes a aceder aos mesmos dados simultaneamente, obtendo, consequentemente, informação corrompida. Mais ainda, apresentamos uma solução que garante exclusão mútua entre um escritor e vários leitores, usando o protocolo NBW, com a adaptação de que o facto de sabermos a priori o período dos processos, permite-nos eliminar os ciclos de "leitura e verificação" do algoritmo original.
verificação de modelos, verificação formal, sistemas em tempo-real, sistemas distribuídos, IMA

Novembro 17, 2017, 10:0

Publicação

Obra sujeita a Direitos de Autor

Orientação

ORIENTADOR

Paulo Alexandre Carreira Mateus

Departamento de Matemática (DM)

Professor Associado