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

Mostrar outras versões (1)

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 an...

ver descrição completa

Na minha lista:
Detalhes bibliográficos
Autor principal: Galvão, Stephenson de Sousa Lima
Outros Autores: Déharbe, David Boris Paul
Formato: Dissertação
Idioma:por
Publicado em: Universidade Federal do Rio Grande do Norte
Assuntos:
Especificação
FreeRTOS
Método B
Specification
B method
CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO
Endereço do item:https://repositorio.ufrn.br/jspui/handle/123456789/18021
Tags: Adicionar Tag
Sem tags, seja o primeiro a adicionar uma tag!
id ri-123456789-18021
record_format dspace
spelling ri-123456789-180212017-11-04T13:37:30Z Especificação do micronúcleo FreeRTOS utilizando o método B Galvão, Stephenson de Sousa Lima Déharbe, David Boris Paul http://lattes.cnpq.br/7644392387532784 http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4768856U5 Oliveira, Marcel Vinicius Medeiros http://lattes.cnpq.br/1756952696097255 Andrade, Aline Maria Santos http://lattes.cnpq.br/0612005197639506 Especificação FreeRTOS Método B Specification FreeRTOS B method CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO 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. 2014-12-17T15:47:55Z 2011-12-07 2014-12-17T15:47:55Z 2011-08-16 masterThesis GALVÃO, Stephenson de Sousa Lima. Especificação do micronúcleo FreeRTOS utilizando o método B. 2011. 117 f. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal do Rio Grande do Norte, Natal, 2011. https://repositorio.ufrn.br/jspui/handle/123456789/18021 por Acesso Aberto application/pdf application/pdf Universidade Federal do Rio Grande do Norte BR UFRN Programa de Pós-Graduação em Sistemas e Computação Ciência da Computação
institution Repositório Institucional
collection RI - UFRN
language por
topic Especificação
FreeRTOS
Método B
Specification
FreeRTOS
B method
CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO
spellingShingle Especificação
FreeRTOS
Método B
Specification
FreeRTOS
B method
CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO
Galvão, Stephenson de Sousa Lima
Especificação do micronúcleo FreeRTOS utilizando o método B
description 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.
author2 Déharbe, David Boris Paul
author_facet Déharbe, David Boris Paul
Galvão, Stephenson de Sousa Lima
format masterThesis
author Galvão, Stephenson de Sousa Lima
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
publisher Universidade Federal do Rio Grande do Norte
publishDate 2014
url https://repositorio.ufrn.br/jspui/handle/123456789/18021
work_keys_str_mv AT galvaostephensondesousalima especificacaodomicronucleofreertosutilizandoometodob
_version_ 1773958303693406208

Registros relacionados