Made available in DSpace on 2014-12-17T15:47:55Z (GMT). No. of bitstreams: 1
StephennsonSLG_DISSERT.pdf: 4909051 bytes, checksum: 2a9f94a42d9fc75bb16a1ff239148437 (MD5)
Previous issue date: 2011-08-16 / This paper presents a contribution to the international Verified Software Repository
effort through the formal specification of the microkernel FreeRTOS real-time system.
Such specification was made in abstract level making use of the B method . For thus,
properties of the microkernel were chosen and selected as specification requisites, which
was constructed centered at the functionalities responsible for the utilization of these properties.
This properties weres setting as specification requirements. The specification was
constructed modeling the function of microkernel that implement this properties. This
work intended to encourage the formal verification of FreeRTOS and also contribute to
the formal creation of a microkernel real-time systems, based in FreeRTOS. Furthermore,
this model brings a formal documentation point view of the microkernel, demonstrating
features and how this internal states is changing. Finally, this work could be an example
of specification of the actual system by the B method. / Este trabalho apresenta uma contribui??o para o esfor?o internacional do Verified
Software Repository atrav?s da especifica??o formal da biblioteca de sistema de tempo
real FreeRTOS. Tal especifica??o foi realizada de forma abstrata utilizando o m?todo
B. Para isso, propriedades disponibilizadas por essa biblioteca foram elencadas e selecionadas
como requisitos da especifica??o, a qual foi constru?da centrada nas funcionalidades
respons?veis pela utiliza??o dessas propriedades. Com a modelagem desenvolvida
pretende-se incentivar a verifica??o formal do FreeRTOS e tamb?m contribuir
para a cria??o formal de uma biblioteca de sistemas de tempo real baseada na FreeRTOS.
Al?m disso, tal modelagem traz uma documenta??o do ponto de vista formal do sistema,
demonstrando como ocorrer internamente o seu funcionamento e serve como um exemplo
da especifica??o de um sistema real pelo m?todo B.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufrn.br:123456789/18021 |
| Date | 16 August 2011 |
| Creators | Galv?o, Stephenson de Sousa Lima |
| Contributors | CPF:00809085437, http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4768856U5, Oliveira, Marcel Vinicius Medeiros, CPF:02386943488, http://lattes.cnpq.br/1756952696097255, Andrade, Aline Maria Santos, CPF:15920763515, http://lattes.cnpq.br/0612005197639506, D?harbe, David Boris Paul |
| Publisher | Universidade Federal do Rio Grande do Norte, Programa de P?s-Gradua??o em Sistemas e Computa??o, UFRN, BR, Ci?ncia da Computa??o |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Format | application/pdf |
| Source | reponame:Repositório Institucional da UFRN, instname:Universidade Federal do Rio Grande do Norte, instacron:UFRN |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0023 seconds