Utilize este identificador para referenciar este registo: http://hdl.handle.net/10400.6/3716
Título: Towards a formally verified microkernel using the Frama-C toolset
Autor: Carloto, Carlos José Abreu Dias da Silva
Orientador: Sousa, Simão Melo de
Palavras-chave: Design by contract
Formal verification
xLuna
Formal methods
Frama-C
Hoare logic
Static verification
Deductive verification
Separation Kernel
Data de Defesa: 2010
Resumo: This dissertation is included in the MSc course in Computer Science of the University of Beira Interior. It is a Formal Method’s related dissertation, where it’s used an Hoare Logic based paradigm, the Design by Contract (DbC). This project consists in doing a Formal Verification of an industrial real-time Operating System (OS) kernel. The OS kernel that is verified is the eXtending free/open-source reaL-time execUtive for oN-board space Applications (xLuna). It is an OS from a portuguese company, CSW. The code that was verified is the real source code of xLuna. More precisely the source code of the Interrupt request (IRQ) Manager module. The platform that was used to do the verification is the FRAmework for Modular Analyses of C (Frama-C) Toolset which is a platform that allows the verification of C code. Some incompatibilities were found in the use of the Frama-C in the source code of the IRQ Manager. Both results and Frama-C incompatibilities will be analyzed in the dissertation.
URI: http://hdl.handle.net/10400.6/3716
Designação: Dissertação apresentada à Universidade da Beira Interior para a obtenção do grau de mestre em Engenharia Informática
Aparece nas colecções:FE - DI | Dissertações de Mestrado e Teses de Doutoramento

Ficheiros deste registo:
Ficheiro Descrição TamanhoFormato 
Dissertação - Carlos José Abreu Dias da Silva Carloto.pdf2,17 MBAdobe PDFVer/Abrir


FacebookTwitterDeliciousLinkedInDiggGoogle BookmarksMySpace
Formato BibTex MendeleyEndnote Degois 

Todos os registos no repositório estão protegidos por leis de copyright, com todos os direitos reservados.