Publication
Towards a formally verified microkernel using the Frama-C toolset
| dc.contributor.advisor | Sousa, Simão Patrício Melo de | |
| dc.contributor.author | Carloto, Carlos José Abreu Dias da Silva | |
| dc.date.accessioned | 2015-07-15T09:44:06Z | |
| dc.date.available | 2015-07-15T09:44:06Z | |
| dc.date.issued | 2010 | |
| dc.date.submitted | 2010 | |
| dc.description.abstract | 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. | por |
| dc.identifier.uri | http://hdl.handle.net/10400.6/3716 | |
| dc.language.iso | eng | por |
| dc.subject | Design by contract | por |
| dc.subject | Formal verification | por |
| dc.subject | xLuna | por |
| dc.subject | Formal methods | por |
| dc.subject | Frama-C | por |
| dc.subject | Hoare logic | por |
| dc.subject | Static verification | por |
| dc.subject | Deductive verification | por |
| dc.subject | Separation Kernel | por |
| dc.title | Towards a formally verified microkernel using the Frama-C toolset | por |
| dc.type | master thesis | |
| dspace.entity.type | Publication | |
| rcaap.rights | openAccess | por |
| rcaap.type | masterThesis | por |
| thesis.degree.discipline | Engenharia Informática | por |
| thesis.degree.level | Mestre | por |
| thesis.degree.name | Dissertação apresentada à Universidade da Beira Interior para a obtenção do grau de mestre em Engenharia Informática | por |
Files
Original bundle
1 - 1 of 1
No Thumbnail Available
- Name:
- Dissertação - Carlos José Abreu Dias da Silva Carloto.pdf
- Size:
- 2.12 MB
- Format:
- Adobe Portable Document Format
- Description:
License bundle
1 - 1 of 1
No Thumbnail Available
- Name:
- license.txt
- Size:
- 1.71 KB
- Format:
- Item-specific license agreed upon to submission
- Description: