Contribuições para melhoria do processo de verificação formal de propriedades em programas AADL

Abstract

projeto de sistemas embarcados criticos exige o uso de metodologias adequadas, visto que falhas no sistema podem causar danos catastroficos. Neste contexto se enquadra o projeto Topcased, o qual propõe uma série de ferramentas capazes de suportar a verificação formal de propriedades. A linguagem AADL tem um papel fundamental neste processo, pois sua utilização permite o emprego da transformação de modelos e a aplicação da verificação formal de propriedades. Entretanto, a especificação das propriedades de verificação e a análise dos seus resultados são ainda topicos em aberto. Esta dissertação visa suprir esta carência propondo um assistente para especificação de propriedades de verificação na linguagem AADL e uma interface para a visualização dos resultados de verificação, juntamente com um simulador de contraexemplos. O assistente construido classica as propriedades em padrões pre-definidos, utilizando uma linguagem natural ao usuário. Para validar as ferramentas desenvolvidas realizou-se um estudo de caso, o qual consistiu da especificação e verificação de propriedades de um sistema de marcapasso. Desta forma, este trabalho contribui com a melhoria da cadeia de verificação da linguagem AADL no escopo do projeto Topcased.