Utilize este identificador para referenciar este registo: http://hdl.handle.net/10400.6/3717
Título: Towards a formally verified microkernel using the VCC verifier
Autor: Tojal, Joaquim José e Silva de Carvalho
Orientador: Sousa, Simão Melo de
Faria, José Miguel
Palavras-chave: Concurrency
Critical system
Design by contract
Embedded systems
Formal verification
Formal methods
Microkernel
Real-time
Operating system
Software reliability
xLuna
Safety
Data de Defesa: 2010
Resumo: In this thesis we present the design by contract modular approach to formal verification of an industrial real-time microkernel which was not designed with formal verification in mind. The microkernel module targeted is a particular interrupt manager of xLuna Real Time Operating System (RTOS) for embedded systems built by Critical Software S.A. The annotations were verified automatically using the Microsoft Research Verified C Compiler (VCC) tool to reason about concurrency and safety properties of xLuna kernel. The specifications are based in Hoare-style pre- and post-conditions inlined with the real code. xLuna is a microkernel based on the RTEMS Real-Time Operating System. xLuna extends RTEMS for run a GNU/Linux Operating System, providing a runtime multitasking environment for real-time (RTEMS) and non-real-time (Linux) applications. xLuna runs in a preemptable and concurrent environment. Therefore, we use VCC for reasoning about concurrent executions and some functional and safety properties of xLuna microkernel. VCC is an automated verifier for concurrent C programs that is being developed by Microsoft Research, Redmond, USA and European Microsoft Innovation Center (EMIC), Aachen, Germany. VCC is being built and used for operating system verification which makes it suitable for our verification work. Specifications were added to xLuna code following a modular approach to the verification of a specific microkernel module, namely the Interrupt Request (IRQ) module. The Verified C Compiler (VCC) annotations added cover approximately 80% of the IRQ manager C code (the remaining 20% of the code are relative to auxiliary functions outside the scope of our verification work). All the annotations were automatically verified and proven to be correct.
URI: http://hdl.handle.net/10400.6/3717
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 
Dissertacao_Joaquim_Tojal.pdf1,76 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.