Especificação do micronúcleo FreeRTOS utilizando o método B /

Mostrar outras versões (1)

Resumo: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 disponibiliza...

ver descrição completa

Na minha lista:

Detalhes bibliográficos
Principais autores:	Galvão, Stephenson de Sousa Lima., Déharbe, David Boris Paul., Universidade Federal do Rio Grande Norte.
Formato:	Dissertação
Publicado em:
Assuntos:	Sistemas de computação - Dissertação. Especificação FreeRTOS - Verified software repository - Sistemas de tempo real FreeRTOS - Método B - Specification FreeRTOS. Verified software repository. Real-time systems FreeRTOS. B method.
Endereço do item:	https://repositorio.ufrn.br/jspui/bitstream/123456789/18021/1/StephennsonSLG_DISSERT.pdf
Tags:	Adicionar Tag Sem tags, seja o primeiro a adicionar uma tag!

id	oai:localhost:123456789-109964
record_format	dspace
spelling	oai:localhost:123456789-1099642022-11-30T18:45:40Z Especificação do micronúcleo FreeRTOS utilizando o método B / Galvão, Stephenson de Sousa Lima. Déharbe, David Boris Paul. Universidade Federal do Rio Grande Norte. Sistemas de computação - Dissertação. Especificação FreeRTOS - Dissertação. Verified software repository - Dissertação. Sistemas de tempo real FreeRTOS - Dissertação. Método B - Dissertação. Specification FreeRTOS. Verified software repository. Real-time systems FreeRTOS. B method. Resumo: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. #$&Abstract: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. 1 2022-10-06T02:24:35Z 2022-10-06T02:24:35Z 2010. Dissertação 004.78 G182m DISSERT 170016 https://repositorio.ufrn.br/jspui/bitstream/123456789/18021/1/StephennsonSLG_DISSERT.pdf https://repositorio.ufrn.br/jspui/bitstream/123456789/18021/1/StephennsonSLG_DISSERT.pdf
institution	Acervo SISBI
collection	SIGAA
topic	Sistemas de computação - Dissertação. Especificação FreeRTOS - Dissertação. Verified software repository - Dissertação. Sistemas de tempo real FreeRTOS - Dissertação. Método B - Dissertação. Specification FreeRTOS. Verified software repository. Real-time systems FreeRTOS. B method.
spellingShingle	Sistemas de computação - Dissertação. Especificação FreeRTOS - Dissertação. Verified software repository - Dissertação. Sistemas de tempo real FreeRTOS - Dissertação. Método B - Dissertação. Specification FreeRTOS. Verified software repository. Real-time systems FreeRTOS. B method. Galvão, Stephenson de Sousa Lima. Déharbe, David Boris Paul. Universidade Federal do Rio Grande Norte. Especificação do micronúcleo FreeRTOS utilizando o método B /
description	Resumo: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. #$&Abstract: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.
format	Dissertação
author	Galvão, Stephenson de Sousa Lima. Déharbe, David Boris Paul. Universidade Federal do Rio Grande Norte.
author_facet	Galvão, Stephenson de Sousa Lima. Déharbe, David Boris Paul. Universidade Federal do Rio Grande Norte.
author_sort	Galvão, Stephenson de Sousa Lima.
title	Especificação do micronúcleo FreeRTOS utilizando o método B /
title_short	Especificação do micronúcleo FreeRTOS utilizando o método B /
title_full	Especificação do micronúcleo FreeRTOS utilizando o método B /
title_fullStr	Especificação do micronúcleo FreeRTOS utilizando o método B /
title_full_unstemmed	Especificação do micronúcleo FreeRTOS utilizando o método B /
title_sort	especificação do micronúcleo freertos utilizando o método b /
publishDate	2022
url	https://repositorio.ufrn.br/jspui/bitstream/123456789/18021/1/StephennsonSLG_DISSERT.pdf
work_keys_str_mv	AT galvaostephensondesousalima especificacaodomicronucleofreertosutilizandoometodob AT deharbedavidborispaul especificacaodomicronucleofreertosutilizandoometodob AT universidadefederaldoriograndenorte especificacaodomicronucleofreertosutilizandoometodob
_version_	1766808735945064448

Especificação do micronúcleo FreeRTOS utilizando o método B /

Registros relacionados