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

AUTOR(ES)

Stephenson de Sousa Lima Galvão

FONTE

IBICT - Instituto Brasileiro de Informação em Ciência e Tecnologia

DATA DE PUBLICAÇÃO

16/08/2011

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.

ASSUNTO(S)

b method especificação freertos método b sistemas de computacao specification freertos

Documentos Relacionados

• Ferramenta visual para especificação de hiperdocumentos, segundo o método OOHDM
• Investigação do potencial genotóxico do clareador caseiro (peróxido de carbamida a 15%) na mucosa bucal utilizando o teste de micronúcleo
• Especificação de sistemas utilizando lógica linear com subexponencias
• Problema de contato com atrito utilizando o metodo do lagrangiano aumentado
• Preservação do inóculo de Plasmodiophora brassicae utilizando o método de congelamento