Document details

Towards a formally verified microkernel using the Frama-C toolset

Author(s): Carloto, Carlos José Abreu Dias da Silva

Date: 2010

Persistent ID:

Origin: uBibliorum

Subject(s): Design by contract; Formal verification; xLuna; Formal methods; Frama-C; Hoare logic; Static verification; Deductive verification; Separation Kernel


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.

Document Type Master thesis
Language English
Advisor(s) Sousa, Simão Patrício Melo de
Contributor(s) Carloto, Carlos José Abreu Dias da Silva
facebook logo  linkedin logo  twitter logo 
mendeley logo

Related documents

No related documents