Return to search

Especifica??o do micron?cleo FreeRTOS utilizando o m?todo B

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.

Identiferoai:union.ndltd.org:IBICT/oai:repositorio.ufrn.br:123456789/18021
Date16 August 2011
CreatorsGalv?o, Stephenson de Sousa Lima
ContributorsCPF: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
PublisherUniversidade 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 SetsIBICT Brazilian ETDs
LanguagePortuguese
Detected LanguageEnglish
Typeinfo:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis
Formatapplication/pdf
Sourcereponame:Repositório Institucional da UFRN, instname:Universidade Federal do Rio Grande do Norte, instacron:UFRN
Rightsinfo:eu-repo/semantics/openAccess

Page generated in 0.0023 seconds