Navegando por Autor "Galvão, Stephenson de Sousa Lima"
Agora exibindo 1 - 1 de 1
- Resultados por página
- Opções de Ordenação
Dissertação Especificação do micronúcleo FreeRTOS utilizando o método B(Universidade Federal do Rio Grande do Norte, 2011-08-16) Galvão, Stephenson de Sousa Lima; Déharbe, David Boris Paul; ; http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4768856U5; ; http://lattes.cnpq.br/7644392387532784; Oliveira, Marcel Vinicius Medeiros; ; http://lattes.cnpq.br/1756952696097255; Andrade, Aline Maria Santos; ; http://lattes.cnpq.br/0612005197639506Este 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.