| Name: | Description: | Size: | Format: | |
|---|---|---|---|---|
| 2.12 MB | Adobe PDF |
Advisor(s)
Abstract(s)
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.
Description
Keywords
Design by contract Formal verification xLuna Formal methods Frama-C Hoare logic Static verification Deductive verification Separation Kernel