StephennsonSLG-DISSERT

Prévia do material em texto

UNIVERSIDADE FEDERAL DO RIO GRANDE DO NORTE
DEPARTAMENTO DE INFORMÁTICA E MATEMÁTICA APLICADA
PROGRAMA DE PÓS-GRADUAÇÃO EM SISTEMAS E COMPUTAÇÃO
STEPHENSON DE SOUSA LIMA GALVÃO
Especificação do micronúcleo FreeRTOS
utilizando o método B
Dissertação apresentada como requisito parcial
para a obtenção do grau de
Mestre em Ciência da Computação
Prof. Dr. David Boris Paul Déharbe
Orientador
Natal, agosto de 2010
 
 
AGRADECIMENTOS
Agradeço primeiramente à Deus, sem ele nada é possível.
Ao meu pai, pelo incondicional.
À minha mãe, pelo incentivo.
Aos meus irmãos, pelo companheirismo.
À Luanne, pelo carinho e compreensão de amiga, namorada e, brevemente, esposa.
Ao David, por ir além dos livros e ensinar como deve ser um verdadeiro professor.
SUMÁRIO
LISTA DE FIGURAS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
LISTA DE TABELAS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
RESUMO . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
ABSTRACT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
1 INTRODUÇÃO . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
1.1 Objetivo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
1.2 Metodologia . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2 TRABALHOS RELACIONADOS . . . . . . . . . . . . . . . . . . . . . 23
2.1 Trabalhos anteriores . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
2.2 Trabalhos recentes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
2.3 Outros trabalhos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.4 Considerações finais . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3 FREERTOS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3.1 Gerenciamento de tarefas e co-rotinas . . . . . . . . . . . . . . . . . . . 32
3.1.1 Tarefa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
3.1.2 Co-rotinas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
3.1.3 Escalonador de tarefas . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
3.1.4 Biblioteca . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
3.2 Comunicação e sincronização entre tarefas . . . . . . . . . . . . . . . . 39
3.2.1 Fila de Mensagens . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
3.2.2 Semáforo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
3.2.3 Mutex . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
3.2.4 Biblioteca . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
3.3 Utilização prática dos elementos do FreeRTOS . . . . . . . . . . . . . . 43
3.3.1 Utilização da entidade tarefa . . . . . . . . . . . . . . . . . . . . . . . . 43
3.3.2 Utilização da fila de mensagens . . . . . . . . . . . . . . . . . . . . . . . 44
3.3.3 Utilização do semáforo . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
3.3.4 Utilização das co-rotinas . . . . . . . . . . . . . . . . . . . . . . . . . . 47
3.4 Considerações finais . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
4 O MÉTODO B . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
4.1 Etapas do desenvolvimento em B . . . . . . . . . . . . . . . . . . . . . . 49
4.2 Máquina abstrata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
4.2.1 Especificação do estado da máquina . . . . . . . . . . . . . . . . . . . . 52
4.2.2 Especificação das operações da máquina . . . . . . . . . . . . . . . . . . 52
4.3 Obrigações de prova . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
4.3.1 Consistência do invariante . . . . . . . . . . . . . . . . . . . . . . . . . . 57
4.3.2 Obrigação de prova da inicialização . . . . . . . . . . . . . . . . . . . . 58
4.3.3 Obrigação de prova das operações . . . . . . . . . . . . . . . . . . . . . 58
4.4 Refinamento . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
4.4.1 Refinamento do estado . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
4.4.2 Refinamento das operações . . . . . . . . . . . . . . . . . . . . . . . . . 60
4.4.3 Obrigação de prova do refinamento . . . . . . . . . . . . . . . . . . . . . 60
4.5 Considerações finais . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
5 ESCOPO DA ESPECIFICAÇÃO . . . . . . . . . . . . . . . . . . . . . . 63
5.1 Escopo da especificação . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
5.1.1 Tarefas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
5.1.2 Escalonador . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
5.1.3 Fila de mensagens . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
5.1.4 Semáforo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
5.1.5 Mutex . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
5.2 Considerações finais . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
6 MODELAGEM ABSTRATA . . . . . . . . . . . . . . . . . . . . . . . . . 67
6.1 Arquitetura da especificação . . . . . . . . . . . . . . . . . . . . . . . . 67
6.1.1 Organização . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
6.1.2 Finalidade dos módulos . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
6.1.3 Relação entre os módulos . . . . . . . . . . . . . . . . . . . . . . . . . . 68
6.2 Tipos e configurações do sistema . . . . . . . . . . . . . . . . . . . . . . 69
6.2.1 Tipos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
6.2.2 Configurações . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
6.3 Tarefa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
6.3.1 Estado . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
6.3.2 Operações . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72
6.4 Escalonador . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
6.4.1 Estado . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
6.4.2 Operações . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
6.5 Fila de mensagens . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
6.5.1 Estado . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
6.5.2 Operações . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
6.6 Semáforo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
6.6.1 Estado . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
6.6.2 Operações . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
6.7 Mutex . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
6.7.1 Estado . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85
6.7.2 Operações . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
6.8 Funcionalidades . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88
6.8.1 Máquina FreeRTOSBasic . . . . . . . . . . . . . . . . . . . . . . . . . . 88
6.8.2 Máquina FreeRTOS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92
6.9 Obrigações de prova . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94
6.10 Considerações finais . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96
7 REFINAMENTO DA MODELAGEM . . . . . . . . . . . . . . . . . . . . 97
7.1 Refinamento de prioridade de uma tarefa . . . . . . . . . . . . . . . . . 97
7.1.1 Estado do Task_priority . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
7.1.2 Operações . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98
7.2 Refinamento do conjunto de mensagens de uma fila de mensagens . . . 101
7.2.1 Estado . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102
7.2.2 Operações . . . . . . . . . . . .. . . . . . . . . . . . . . . . . . . . . . 102
7.3 Refinamento do tempo de bloqueio de uma tarefa . . . . . . . . . . . . . 105
7.3.1 Estado . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
7.3.2 Operações . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
7.4 Refinamento do estouro de tempo do escalonador . . . . . . . . . . . . . 107
7.4.1 Estado . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
7.4.2 Operações . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
7.5 Considerações finais . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110
8 CONCLUSÕES . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111
8.1 Trabalhos futuros . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112
8.2 Limitações da método B . . . . . . . . . . . . . . . . . . . . . . . . . . . 113
REFERÊNCIAS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115
LISTA DE FIGURAS
1.1 Esboço da arquitetura da especificação. . . . . . . . . . . . . . . . . 20
2.1 Camadas da especificação do UCLA (POPEK et al., 1979) . . . . . . 24
2.2 Mapeamento de estado entre níveis de abstração.(POPEK et al., 1979) 24
2.3 Camadas da especificação do PSOS.(FEIERTAG; NEUMANN, 1979) 25
2.4 Módulos da especificação do L4.(KOLANSKI; KLEIN, 2006) . . . . 26
2.5 Processo de projeto do seL4.(KLEIN et al., 2009) . . . . . . . . . . . 27
2.6 Camadas de refinamento do seL4.(KLEIN et al., 2009) . . . . . . . . 27
3.1 Camada abstrata proporcionada pelo FreeRTOS.(Richard Barry, 2009a) 31
3.2 Diagrama de estados de uma tarefa no FreeRTOS.(Richard Barry,
2009a) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
3.3 Grafo de estados de uma co-rotina.(Richard Barry, 2009a) . . . . . . 35
3.4 Funcionamento de um escalonador preemptivo baseado na prioridade. 36
3.5 Funcionamento de uma fila de mensagens. . . . . . . . . . . . . . . . 39
3.6 Diagrama de estado do semáforo com contador. . . . . . . . . . . . . 41
3.7 Funcionamento do mecanismo de herança de prioridade. . . . . . . . 42
3.8 Estrutura da rotina de uma tarefa (Richard Barry, 2009a). . . . . . . . 43
3.9 Aplicação formada por uma tarefa cíclica (Richard Barry, 2009a). . . 44
3.10 Aplicação que utiliza uma fila de mensagens (Richard Barry, 2009a). 45
3.11 Aplicação que demonstra a utilização de um semáforo (Richard Barry,
2009a). . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
3.12 Modelo da rotina de execução de uma co-rotina (Richard Barry, 2009a). 47
3.13 Aplicação que demonstra a utilização de uma co-rotina (Richard Barry,
2009a). . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
4.1 Etapas do desenvolvimento de sistema através do método B (Bartira
Dantas et al., 2008a). . . . . . . . . . . . . . . . . . . . . . . . . . . 50
4.2 Exemplo da máquina abstrata Kernel. . . . . . . . . . . . . . . . . . 51
4.3 Operação que consulta se uma tarefa pertence à máquina Kernel . . . 52
4.4 Operação inclui uma nova tarefa na máquina Kernel . . . . . . . . . 53
4.5 Operação que cria uma tarefa aleatéria na máquina Kernel . . . . . . 56
4.6 Operação que informa a situação do conjunto task na máquina Kernel . 57
4.7 Refinamento da máquina abstrata Kernel . . . . . . . . . . . . . . . . 60
6.1 Esbouço da arquitetura da especificação. . . . . . . . . . . . . . . . . 68
6.2 Especificação de tipos do módulo Types . . . . . . . . . . . . . . . . 69
6.3 Especificação do módulo FreeRTOSConfig . . . . . . . . . . . . . . 70
6.4 Especificação do estaod de uma tarefa no módulo Task . . . . . . . . 71
6.5 Especificação da operação t_create. . . . . . . . . . . . . . . . . . . 72
6.6 Especificação da operação t_delayTask . . . . . . . . . . . . . . . . . 73
6.7 Especificação da operação t_resume. . . . . . . . . . . . . . . . . . 74
6.8 Especifacação da parte do estado da máquina relacionada ao Task . . . 74
6.9 Operação t_yield . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
6.10 Operação t_startScheduler . . . . . . . . . . . . . . . . . . . . . . . 76
6.11 Operação t_incrementTick . . . . . . . . . . . . . . . . . . . . . . . 77
6.12 Operação t_resumeAll . . . . . . . . . . . . . . . . . . . . . . . . . 77
6.13 Operação t_resumeAll . . . . . . . . . . . . . . . . . . . . . . . . . 78
6.14 Operação t_resumeAll . . . . . . . . . . . . . . . . . . . . . . . . . 79
6.15 Operação q_queueCreate. . . . . . . . . . . . . . . . . . . . . . . . 81
6.16 Operação q_sendItem. . . . . . . . . . . . . . . . . . . . . . . . . . 82
6.17 Operação q_insertTaskWaitingToReceive. . . . . . . . . . . . . . . 82
6.18 Operação q_insertTaskWaitingToReceive. . . . . . . . . . . . . . . 83
6.19 Operação q_createSemaphore. . . . . . . . . . . . . . . . . . . . . 84
6.20 Operação q_takeSemaphore. . . . . . . . . . . . . . . . . . . . . . 85
6.21 Parte da máquina Queue que especifica o mutex. . . . . . . . . . . . 85
6.22 Operação q_createMutex . . . . . . . . . . . . . . . . . . . . . . . . 87
6.23 Operação q_takeMutex . . . . . . . . . . . . . . . . . . . . . . . . . 87
6.24 Operação t_priorityInherit . . . . . . . . . . . . . . . . . . . . . . . 88
6.25 Estado da máquina FreeRTOSBasic. . . . . . . . . . . . . . . . . . 89
6.26 Funcionalidade vTaskDelay . . . . . . . . . . . . . . . . . . . . . . . 91
6.27 Funcionalidade xTaskResumeAll . . . . . . . . . . . . . . . . . . . . 92
6.28 Operação sendIten. . . . . . . . . . . . . . . . . . . . . . . . . . . 93
6.29 Funcionalidade xQueueSendToFront . . . . . . . . . . . . . . . . . . 94
6.30 Funcionalidade xQueueSendToBack . . . . . . . . . . . . . . . . . . 94
6.31 Tela da obrigação de prova interativa da ferramenta Atelier B. . . . . 95
7.1 Estado Task_priority . . . . . . . . . . . . . . . . . . . . . . . . . . 98
7.2 Refinamento da operação t_create. . . . . . . . . . . . . . . . . . . 99
7.3 Refinamento da operação t_create. . . . . . . . . . . . . . . . . . . 100
7.4 Refinamento da operação t_priorityInherit . . . . . . . . . . . . . . 101
7.5 Refinamento da operação t_setPriority . . . . . . . . . . . . . . . . . 101
7.6 Estado do refinamento Queue_r . . . . . . . . . . . . . . . . . . . . 102
7.7 Continuação do invariante do refinamento Queue_r . . . . . . . . . . 103
7.8 Parte do refinamento da operaçãomathitq_sendItem. . . . . . . . . 104
7.9 Parte do refinamento da operaçãomathitq_takeSemaphore. . . . . 104
7.10 Parte do refinamento da operação q_takeMutex . . . . . . . . . . . . 104
7.11 Parte do refinamento da operação q_takeMutex . . . . . . . . . . . . 105
7.12 Refinamento do tempo de bloqueio da operação t_delayTask . . . . . 106
7.13 Refinamento do tempo de bloqueio da operação t_resumeAll . . . . . 106
7.14 Refinamento do tempo de bloqueio da operação t_beforeResumeAll . 107
7.15 Estado do refinamento Task_overflow . . . . . . . . . . . . . . . . . 108
7.16 Refinamento de tempo de estouro da operação t_delayTask . . . . . . 109
7.17 Refinamento de tempo de estoura da operação t_incrementTick . . . 109
8.1 Função executada quando a tarefa associada a ela entrar em execução 113
8.2 Técnica que controla as atribuições paralelas em B. . . . . . . . . . . 114
LISTA DE TABELAS
6.1 Tabela dos módulos criados na modelagem abstrata. . . . . . . . . . 96
7.1 Tabela dos módulos gerados no refinamento. . . . . . . . . . . . . . 110
8.1 Tabela dos módulos criados na modelagem do FreeRTOS. . . . . . . 112
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 sele-
cionadas como requisitos da especificação, a qual foi construída centrada nas funcio-
nalidades responsáveis pela utilização dessas propriedades. Com a modelagem desen-
volvida pretende-se incentivar a verificação formaldo 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.
Palavras-chave: Especificação, FreeRTOS, 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 prop-
erties. 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.
Palavras-chave: Specification, FreeRTOS, B method.
17
1 INTRODUÇÃO
A Ciência da Computação é uma área relativamente jovem, mas com grande im-
pacto na sociedade atual. Através dela, é possível acelerar-se anos de desenvolvimento e
pesquisas das demais áreas da ciência, como no mapeamento do genoma humano. De-
vido a isso, em (COMMITTEE, 2005) ela chegou a ser citada como um dos pilares da
ciência, considerada também como um fator crucial para a economia, tecnologia e desen-
volvimento de um país.
Ciente dessa importância, pesquisadores de todo o mundo têm buscado reunir esforços
em torno de objetivos comuns, definindo diretrizes a serem seguidas pela computação, ao
longo dos próximos anos. Essas diretrizes são estabelecidas visando suprir as necessi-
dades mais relevantes da sociedade atual, as quais, em geral, são obstáculos ainda não
vencidos pela computação, e, por isso, denominados como “Grandes Desafios da Com-
putação”
Seguindo esse contexto, a Sociedade Brasileira de Computação (SBC) listou, em
(SBC, 2006), alguns desses principais desafios, dentre os quais está o desafio de de-
senvolvimento tecnológico de qualidade: sistemas disponíveis, corretos, seguros, es-
caláveis, persistentes e ubíquos. Esse desafio visa à pesquisa de métodos, técnicas, mod-
elos, dispositivos e padrões de projeto capazes de auxiliar os projetistas e desenvolve-
dores de grandes sistemas de software e hardware a criarem produtos mais previsíveis,
escalonáveis e seguros.
A inspiração para o desenvolvimento tecnológico de qualidade veio principalmente da
crescente utilização de sistemas de computação, no cotidiano, em eletrodomésticos, celu-
lares, carros, metrôs, aviões e salas de cirurgia. Alguns desses são sistemas relativamente
simples e não causam grandes problemas em caso de falhas; outros, são críticos e uma
falha pode levar a conseqüências catastróficas. Para esses últimos, o desenvolvimento de
sistemas fidedignos é de extrema importância.
Entre as abordagens de construção de sistemas fidedignos estão os métodos formais.
Métodos formais são técnicas matemáticas usadas para a análise e verificação de sistemas
de hardware e software. Em particular, eles permitem que propriedades do sistema sejam
declaradas em um modelo matemático passível de validação (RUSHBY, 1993). Devido a
isso, a utilização dessas técnicas na construção de sistema reduz bastante os seus erros de
especificação, projeto e código. Contudo, devido às limitações de ferramentas, compli-
cadas notações e pouco incentivo educacional, os métodos formais têm sido utilizados de
forma tímida pela indústria. Pontualmente, essa abordagem é utilizada em sistemas críti-
cos no projeto astree (COUSOT, 2010), onde sistemas de tempo real embarcados, escrito
em C, como o software de controle do Airbus A380, são verificados estaticamente.
Igualmente à SBC, estudiosos dos métodos formais também elencaram desafios rela-
cionados a esta abordagem, entre os quais está o projeto do “Software Verificado”(J.C.
18
Bicarregui; C.A.R. Hoare; J.C.P. Woodcock, 2008). O Software Verificado é um conjunto
de teorias, ferramentas e experiências usadas para verificação e validação de software. Ele
tem como objetivo aplicar técnicas existentes a sistemas significativos como marcapasso,
mondex e memórias flash para identificar limites, comparar as capacidades e acelerar o
amadurecimento das tecnologias de verificação de software. Um ponto importante desse
projeto foi a criação do seu repositório, onde são armazenadas a utilização de diferentes
abordagens de verificação aplicadas a estudos de casos propostos pelo projeto, sendo o
FreeRTOS um deles (Tony Hoare; Jay Misra, 2005)(Jim Woodcock et al., 2009).
O projeto FreeRTOS (Richard Barry, 2009a)(Richard Barry, 2009b) é uma biblioteca
de funções e tipos para a construção de sistemas de tempo real. Suas características
são: popularidade, simplicidade e portabilidade. Atualmente o seu repositório(BARRY,
2010) possui uma taxa maior que 6.000 downloads por mês; o seu código é acessível,
aberto e pequeno. São aproximadamente 2.200 linhas com funções comuns à maioria dos
sistemas operacionais. Além disso, ele é oficialmente suportado por 17 arquiteturas de
microcontroladores diferentes. Unindo essas características ao fato de que o micronúcleo
FreeRTOS é especialmente projetado para desenvolver sistemas embarcados1, a especifi-
cação dessa biblioteca será uma contribuição para a ciência da computação, em especial
a comunidade de métodos formais, pois sistemas fundamentados nesse micronúcleo terão
um grau de fidegnidade maior.
A importâncias dos micronúcleos para um sistema e a utilização da especificação for-
mal em projeto de software já foram anteriormente notadas por Craig em (Iain D. Craig,
2006). Primeiramente, ele afirma que a parte mais importante de um sistema é o seu
micronúcleo, que gerencia os recursos utilizados pela aplicação, sendo este, há tempos,
relacionado com os métodos formais, principalmente para a especificação das operações
de fila. Por fim, ele defende a especificação formal como uma prática de suma importân-
cia a ser realizada antes da codificação, pois através dela o sistema pode ser analisado
de forma abstrata como uma entidade matemática. Assim, propriedades importantes do
sistema podem ser provadas antes da sua codificação, o que diminui os riscos do projeto.
Uma das abordagens formais candidata à especificação do FreeRTOS é o método
B(SCHNEIDER, 2001)(ABRIAL, 1996). O método B é uma metodologia de especifi-
cação, validação e construção de sistemas. Nele, o sistema é inicialmente modelado em
uma linguagem matemática organizada por seções de conteúdo definido e, em seguida,
são geradas várias obrigações de prova para comprovar a coerência desse modelo. Inclu-
sive, para facilitar o desenvolvimento de sistemas, ele dispõe dos mecanismos de mod-
ularização e refinamento, sendo esse último capaz de refinar uma especificação até um
nível algoritmo, passível de transformação para as linguagens de programação imperati-
vas. Por fim, o método B é apoiado por um pacote de ferramentas que suportam todos
os seus ciclos de desenvolvimento, fator crucial para a utilização dessa abordagem nesta
especificação do FreeRTOS.
Em suma, a especificação formal do FreeRTOS através do método B, além de ser
um esforço para a resolução dos desafios apresentados, é uma grande contribuição para a
computação, principalmente a comunidade de métodos formais. Tal especificação poderá
ainda agregar valor e confiança ao micronúcleo, servindo também como documentação
e entrada para técnicas de teste de sistemas construídosatravés do FreeRTOS(E. Jaffuel;
B. Legeard, 2007). Além disso, devido à utilização do método B em um caso de uso
real, esse trabalho poderá apresentar problemas de limitações do método B, assim como
1Sistemas com limitações de processamento e memória que estão presentes nos objetos do nosso dia a
dia como carro, avião, televisão, celulares e eletrodomésticos.
19
servir de especificação inicial para a criação de um novo micronúcleo, fundamentada no
FreeRTOS, igualmente ao projeto (KLEIN et al., 2009), comentado na seção 2.2.
Prosseguindo nessa introdução, tem-se, na seção 1.1, o objetivo a ser atingido com
esse trabalho, e na seção 1.2, a metodologia para atingir tal objetivo. Após isso, o capí-
tulo 2 apresenta os trabalhos relacionados a essa proposta. As fundamentações teóricas
referentes ao FreeRTOS e ao método B são apresentadas, respectivamente, nos capítu-
los 3 e 4. O escopo da especificação é demonstrando no capítulo 5. Em seguida, a parte
do inicial da especificicação é demonstrada no capítulo 6 e os refinamentos da mesma
são explicados no capítulo 7. Por último, tem-se a conclusão com os trabalhos futuros no
capítulo 8.
1.1 Objetivo
O objetivo deste trabalho é, através da especificação do FreeRTOS em B, contribuir
para os desafios do software verificado e da construção de sistemas fidedignos. A especi-
ficação desenvolvida modelará funcionalmente, de acordo com a documentação, algumas
das principais funcionalidades que compõem o FreeRTOS, abstraindo detalhes de alo-
cação de memória, controle de concorrência e características relacionadas ao elemento
co-rotina. Ao final, tal especificação será capaz de analisar propriedades estáticas das
funcionalidades. Bem como, a continuação desse trabalho será possível implementar um
micronúcleo de tempo real, fundamentado na documentação do FreeRTOS, criado a partir
de uma especificação em B.
1.2 Metodologia
A metodologia utilizada no desenvolvimento deste trabalho pode ser sucintamente
resumida pelos itens abaixo, os quais serão comentados nos parágrafos seguintes:
• Estudo do método B;
• Estudo do FreeRTOS;
• Elaboração de um plano para a modelagem funcional do FreeRTOS;
• Criação de uma modelagem abstrata;
• Refinamento da modelagem desenvolvida;
• Análise da modelagem desenvolvida;
Por ter sido o método B o formalismo escolhido para o desenvolvimento da mode-
lagem proposta, o primeiro passo desse trabalho foi o estudo sobre essa abordagem. Du-
rante essa pesquisa, vários estudos de caso foram desenvolvidos, entre eles uma especifi-
cação do microcontrolador 8051 (melhor detalhada em (Valério Medeiros Jr.; Stephenson
Galvão, 2008)). Além disso, com o conhecimento adquirido, foi possível colaborar com
os seguintes trabalhos (Bartira Dantas et al., 2008a) e (Bartira Dantas et al., 2008b), nos
quais uma extensão para o método B a nível de assembler é desenvolvida.
O estudo sobre o FreeRTOS foi divido em duas partes principais: a pesquisa na docu-
mentação do sistema e a análise do código fonte do mesmo. Essas partes serão detalhadas
nos parágrafos seguintes.
20
No estudo da documentação do sistema, os principais requisitos, funcionalidades e
características do FreeRTOS puderam ser identificados e classificados de acordo com a
sua importância. Esse trabalho serviu como base para a análise do código fonte e para a
elaboração do plano de desenvolvimento de uma modelagem funcional do sistema.
Durante a análise do código fonte, foi possível, além de validar o explicado na docu-
mentação, identificar a arquitetura do sistema e como suas principais abstrações de hard-
ware e funcionalidades são implementadas. Nessa análise, percebeu-se que, muitas vezes,
o sistema possui detalhes em níveis de assemblagem, o que, segundo Dantas, em (Bartira
Dantas et al., 2008b), também podem ser tratados utilizando o método B.
Através do estudo do FreeRTOS descobriu-se que, apesar dele ser um sistema simples
e pequeno, a sua modelagem é um trabalho que leva muito tempo e esforço. Além disso,
limitações existentes no método B impedem a sua completa especificação. Assim, para o
melhor aproveitamento do modelo desenvolvido, foi elaborado um plano de trabalho para
decidir como e quando os principais elementos e funcionalidades seriam adicionados à
especificação.
No plano de trabalho, determinou-se que a especificação do sistema seria feita em
etapas. Desse modo, as entidades escolhidas e suas características foram acrescentadas
de forma incremental, amadurecendo a especificação.
Com a modelagem abstrata do sistema, foi iniciada a especificação das funcionali-
dades do FreeRTOS. Essa especificação utiliza os mecanismo de composição do método
B, ficando sua arquitetura resumidamente demonstrada pela figura 1.1. Nesse modelo,
o sistema foi divido em quatro módulos principais, nos quais os módulos mais abaixo
fornecem operações e implementam elementos para os módulos superiores realizarem
suas funções, sendo o módulo FreeRTOS responsável por especificar as funcionalidades
do sistema.
Figura 1.1: Esboço da arquitetura da especificação.
Como previsto no plano de trabalho, a modelagem abstrata foi feita de forma in-
cremental. Inicialmente essa modelagem tratou apenas dos elementos tarefa e fila de
mensagens, sendo os demais elementos, semáforo e mutex, especificados em incremen-
tos da modelagem inicial. Outra característica dessa modelagem foi a abstração das pro-
priedades prioridade de uma tarefa, tamanho de uma fila de mensagens, tempo de bloqueio
e estouro de tempo, as quais são adicionadas na etapa de refinamento da modelagem.
Ao total, na especificação abstrata, foram criadas 2.048 linhas, que geraram 1734 obri-
gações de prova (seções 4.3). Entre essas obrigações de prova, somente 361 necessitaram
da interação humana para sua resolução, sendo as demais provadas automaticamente pela
ferramenta adotada pelo projeto, AtelierB. Como resultado dessa etapa foi publicado o
seguinte documento (David Déharbe; Stephenson Galvão; Anamaria Moreira, 2009).
21
Para adicionar as propriedades excluídas da modelagem abstrata (prioridade de uma
tarefa, tamanho de uma fila de mensagens, tempo de bloqueio e estouro de tempo), o re-
finamento da modelagem abstrata adicionou, de forma incremental, quatro novos módu-
los à especificação, um para cada característica tratada. Juntos, esses módulos somaram
1609 linhas de código à especificação e geraram 1717 obrigações de prova, das quais
464 necessitaram ser provadas interativamente, o que fez dessa etapa a mais demorada e
trabalhosa dessa dissertação. Como resultado dessas etapas, uma especificação significa-
tiva do FreeRTOS foi criada. Nela, funcionalidades do sistema puderam ser modeladas
e verificadas. Além disso, tal especificação servirá como material de apoio ao FreeR-
TOS, gerando uma documentação do sistema no ponto de vista formal, na qual alguns
detalhes de incoerência são enfatizados. Em adição, o modelo desenvolvido poderá ser
refinado para o nível algorítmico, possibilitando a criação de um micronúcleo de tempo
real especificado em B e inspirado no FreeRTOS.
22
23
2 TRABALHOS RELACIONADOS
Vários trabalhos anteriores tiveram o objetivo de especificar e verificar micronúcleos
de sistemas. Tal interesse teve início ainda na década de 70 com os projetos UCLA,
PSOS e KIT, explicados na seção 2.1. Nesses trabalhos, as principais contribuições foram
as técnicas utilizadas para a especificação dos sistemas propostos e a prova de que a
verificação formal de sistemas operacionais é um escopo viável.
Recentemente, outros trabalhos também continuaram com o objetivo de especificação
e verificação de micronúcleos. Entre eles, destacam-se o projeto VFiasco, Coyoto, Verisof
e o Verificação do L4, comentados na seção 2.2. Devido à disponibilidade de ferramentas
e ao amadurecimento das abordagens, esses trabalhos tiveram um sucesso maior que seus
precursores. A prova disso está na criação do primeiro micronúcleo de propósito geral,
totalmente verificado e especificado formalmente, desenvolvido no projeto Verificaçãodo
L4.
2.1 Trabalhos anteriores
Alguns dos trabalhos pioneiros na especificação e verificação de micronúcleo, que
terminaram com sucesso, de acordo com os seus objetivos, foram: (POPEK et al., 1979),
(FEIERTAG; NEUMANN, 1979) e (BEVIER, 1989). Esses trabalhos foram realizados
entre os anos de 1970 e 1980 e, apesar dos seus êxitos, nenhum deles produziu um mi-
cronúcleo com uma implementação completamente provada. A seguir, tem-se em detal-
hes cada um desses projetos.
Em (POPEK et al., 1979), Popek documenta a especificação e validação do UCLA
Secure Data Unix, sistema operacional utilizado pelas aplicações no computador DEC
PDP-11/45. Nesse trabalho, os esforços de verificação foram focados no núcleo do sis-
tema, que provê serviços semelhantes aos atuais micronúcleos, como tarefas e paginação.
Além disso, o projeto foi um dos primeiros a separar política do sistema operacional,
como permissões de acesso, do mecanismo do núcleo do sistema, como acesso a memória
física, o que facilitou a verificação do mesmo.
No trabalho de Popek, várias lições foram aproveitadas nessa dissertação. Inicial-
mente, ele dividiu a sua especificação em camadas iguais às da figura 2.1, na qual a única
diferença entre elas está no nível de abstração. Assim, cada camada provê todos os detal-
hes do sistema em níveis de abstrações diferentes. Por exemplo, o nível de código possui
todas as funcionalidades da especificação de nível alto, responsável pela chamadas de
funções do sistema, mas utiliza menos estruturas abstratas que as camadas superiores da
especificação, como listas e conjuntos.
A prova da coerência entre as camadas do UCLA foi feita, como demonstra a figura 2.2,
através do mapeamento de estados. Nesta, cada camada pode ser representada como uma
24
Figura 2.1: Camadas da especificação do UCLA (POPEK et al., 1979)
.
máquina de estado com um conjunto de estados e suas transições. Assim, para garantir a
coerência entres as camadas, cada máquina abstrata deve simular a camada ligeiramente
mais concreta. Essa propriedade é garantida com uma função que mapeia os estados
do nível concreto com os estados do nível abstrato, representada pelas setas verticais da
figura 2.2. Apesar de não ser classificada como esse termo, por seus autores, a técnica
utilizada por Popek foi o refinamento formal (ROEVER; ENGELHARDT, 2008), mais
especificamente, refinamento de dados.
Figura 2.2: Mapeamento de estado entre níveis de abstração.(POPEK et al., 1979)
No (FEIERTAG; NEUMANN, 1979), o sistema PSOS foi projetado. Esse trabalho foi
de maior escopo que o UCLA, pois, além de especificar o núcleo do sistema operacional,
suas regras e hardware também foram tratados. Sua grande contribuição foi a diferente
divisão de camadas do projeto do sistema. As camadas mais baixas criam funcionalidades
para as camadas superiores. Ao total, foram desenvolvidas 17 camadas, como demonstra
a figura 2.3, sendo as 6 inferiores projetadas para serem implementadas no hardware.
Para projetar o PSOS, inicialmente foi criada uma linguagem de especificação e sen-
tenças chamada SPECIAL. Essa linguagem foi utilizada para especificar formalmente os
módulos do sistema, que formavam as suas camadas. SPECIAL também permitia o ma-
peamento de funções e implementações abstratas, relacionando módulos entre níveis.
Vale ressaltar que, apesar das várias tentativas, os trabalhos anteriores foram dificulta-
dos pelo número de mecanismos, como abordagem e ferramentas apropriadas disponíveis
na época. Assim, enquanto o projeto era formalizado, a sua completa verificação de prova
não era desenvolvida. De acordo com Klein, em (KLEIN, 2009), apenas vinte por cento
do UCLA foi provado e o projeto PSOS não foi provado.
25
Figura 2.3: Camadas da especificação do PSOS.(FEIERTAG; NEUMANN, 1979)
Diferente dos trabalhos comentados, (BEVIER, 1989) se destaca por ser o primeiro
trabalho a especificar e provar formalmente o micronúcleo de um Sistema Operacional.
O sistema especificado foi o KIT, um micronúcleo simples e com menos abstrações de
hardware que os micronúcleos modernos. Em seu trabalho, Bevier conseguiu a taxa de
cem por cento de verificação e prova da especificação.
Nesse contexto, a principal contribuição dos trabalhos aqui comentados, foi a ini-
ciativa de especificar sistemas operacionais mostrando que, pelo menos em princípio, é
possível criar um sistema operacional especificado e verificado formalmente.
2.2 Trabalhos recentes
Entre os trabalhos recentes de especificação de sistemas operacionais tem-se os pro-
jetos VFiasco, o Coyotos, o Verisoft e o Verificação do L4.
VFiasco(HOHMUTH; TEWS; STEPHENS, 2002) é um projeto de especificação for-
mal do Fiasco, uma implementação mais simples do micronúcleo L4. Um trabalho im-
portante desse projeto foi listar alguns dos problemas cruciais da verificação dos moder-
nos micronúcleos. Entre esses problemas, está a falta de uma linguagem de implemen-
tação com uma semântica de precisão formal e a complexidade da memória de execução
do núcleo, pois é ele roda diretamente no hardware, não dispondo de mecanismo como
memória virtual.
Outra contribuição do projeto VFiasco foi o desenvolvimento de uma memória virtual
de comportamento bem definido, sobre a qual o sistema é executado, pois as memórias
de hardware não possuem comportamento especificado, o que dificulta a verificação do
sistema. Dessa forma, tal solução poderá ser aproveitada na especificação formal dos
demais sistemas operacionais, que também são executados diretamente no hardware em
memórias de comportamento não previsível.
No projeto Coyotos (SHAPIRO et al., 2004) foi desenvolvida uma implementação
formal para o sucessor do micronúcleo ERO, o Coyoto. Uma das características centrais
desse projeto foi a criação de uma nova linguagem de programação para a implementação
do núcleo, a BitC. Essa linguagem teve como objetivos ser segura, clara e passível de
verificação e foi desenvolvida agrupando características das pesquisas existentes.
Em seguida, tem-se o projeto Verisoft que é um esforço para verificação de toda uma
pilha de sistemas, a qual varia de hardware até aplicações, passando por compiladores e
26
micronúcleos. Nesse projeto, encontra-se a especificação formal do micronúcleo simpli-
ficado VAMOS.
Por último, e mais interessante, é o projeto de especificação e verificação do L4,
um micronúcleo simples e pequeno. Um dos trabalhos desenvolvidos nesse projeto foi
o (KOLANSKI; KLEIN, 2006), que bastante se parece com o proposto nessa disser-
tação, por especificar formalmente a API de um micronúcleo na visão do sistema. Dessa
maneira, as chamadas das funções do núcleo podem ser representadas como alterações no
estado do núcleo, sendo este formado pelas abstrações de hardware do sistema.
Outro ponto comum entre o trabalho anterior e esta especificação é a abordagem for-
mal utilizada, o método B. Além disso, como neste trabalho, Kolanski organizou sua es-
pecificação em módulos responsáveis pelas abstrações de hardware do sistema, os quais
inteligam-se através do mecanismo de inclusão do método B. A estratégia utilizada por
Kolanski pode ser visualizada na figura 2.4, onde as setas demonstram as relações exis-
tentes entre os módulos.
Figura 2.4: Módulos da especificação do L4.(KOLANSKI; KLEIN, 2006)
As diferenças entre os micronúcleos L4 e FreeRTOS estão principalmente nas finali-
dades dos sistemas. O L4 é núcleo de uso genérico que possui as abstrações de hardware
tarefas, memória virtual e IPC, sendo que existem cinco tipos especiais de tarefas. En-
quanto o FreeRTOS serve para a construção de sistemas de tempo real embarcado e possui
as abstrações tarefa, co-rotina, fila de mensagens, semáforo e mutex, as três últimas po-
dem ser consideradas como tipos especiais de comunicação entre processos.
Quanto à especificação dos micronúcleos, os trabalhos divergem em escopo e níveis
de abstração. Na especificação do L4, o modelo desenvolvido possui um escopo mais
abrangente, incluindo políticas de acesso aos recursos e controle de memória.Com isso,
o nível da especificação criada foi bastante abstrato. O FreeRTOS foi especificado par-
cialmente, escopo menor, mas sua especificação atingiu níveis mais concretos.
Além da especificação do L4, o projeto Verificação do L4 desenvolveu um novo sis-
tema, o seL4, com o comportamento totalmente especificado e implementação comple-
tamente comprovada que satisfaz a sua especificação. Desse modo, segundo o Klein em
27
(KLEIN et al., 2009), este foi o primeiro micronúcleo de propósito geral com uma com-
pleta verificação formal.
Figura 2.5: Processo de projeto do seL4.(KLEIN et al., 2009)
Algumas lições da criação do seL4, descrita em (KLEIN et al., 2009), servem como
sugestões para uma completa especificação do FreeRTOS. Inicialmente, em um resumo
sobre especificação de micronúcleo de sistemas, (KLEIN, 2009), Klein relata que o tra-
balho (KOLANSKI; KLEIN, 2006) teve um papel crucial, pois um dos resultados desse
trabalho foi gerar idéias iniciais para o desenho do seL4. Além disso, a constante inte-
gração do desenvolvimento do seL4 e a verificação do L4 proporcionou uma metodolo-
gia que facilitou a ligação da formalização e o protótipo do núcleo, abordagem demon-
strada na figura 2.5. Resumidamente, uma especificação do sistema era desenvolvida
em haskell(BARROS; ALMEIDA, 1998), possibilitando a execução da mesma, por um
simulador de hardware, e a sua verificação formal, através da ferramenta Isabelle/HOL
(NIPKOW; PAULSON; WENZEL, 2002).
Figura 2.6: Camadas de refinamento do seL4.(KLEIN et al., 2009)
A estratégia de verificação formal do projeto do seL4 é minimizada pela figura 2.6.
Praticamente foram criados níveis diferentes de abstrações que vão de uma especifi-
cação abstrata à implementação em C, sendo o nível intermediário uma transformação
28
automática do protótipo em haskell para as asserções da Isabelle/HOL. Cada nível de ab-
stração é formalmente provado que mantém as propriedades do nível superior através de
refinamento, como foi feito no projeto do PSOS.
2.3 Outros trabalhos
Um trabalho que está mais preocupado com concorrência entre processos de uma apli-
cação, mas que deve ser comentado é o de (Moritz Kleine; Steffen Helke, 1999). Nesse
trabalho, a validação de uma aplicação concorrente é feita através da transformação da
linguagem intermediária do compilador LLVM para uma modelagem de baixo nível em
CSP(HOARE, 2004a). Esse modelo é dividido em três partes: Aplicação, onde os com-
portamentos dos processos do sistema são descritos; Domínio, onde os aspectos comuns
do domínio da aplicação são especificados; e Plataforma, onde os detalhes da plataforma
utilizada são formalizados. Um fator positivo dessa divisão é que essa especificação pode
disponibilizar diversas visões do sistema e as partes de domínio e plataforma podem ser
parametrizadas, podendo assim ser reutilizadas em várias aplicações.
Após a criação do modelo CSP, este é analisado através das ferramentas de verifi-
cação, como FDR2 e ProB, que verificam situações de deadlock e condições de corrida
do sistema. Em adição a isso, com a geração do modelo CSP, as atividades implemen-
tadas no sistema são abstraídas para um ponto de vista mais prático e abstrato, permitindo
assim uma melhor análise do sistema.
Por fim, em (Iain D. Craig, 2006) o autor apresenta um guia para a especificação de
sistemas operacionais. Ele demonstra a divisão em camadas de um sistema operacional
convencional, sendo essas: a camada das primitivas de hardware, localizada acima do
hardware; a camada responsável pelo gerenciamento de disco e interrupções de hard-
ware(relógio do sistema); a camada de gerenciamentos de arquivos e controle de inter-
faces; e a camada de chamadas do sistema utilizada pelas aplicações. Essa divisão pro-
porciona uma modelagem incremental de um SO, na qual os elementos mais abstratos e
importantes são tratados inicialmente.
2.4 Considerações finais
Este capítulo teve como objetivo relatar alguns trabalhos existentes de especificação
e verificação formal de sistemas operacionais. Os trabalhos mais antigos foram pioneiros
na formalização de sistemas operacionais, deixando lições para os trabalhos mais recentes
que, devido ao maior suporte de ferramentas e abordagem, tiveram um maior sucesso nos
seus objetivos. Assim, percebe-se que, devido à importância do correto funcionamento
dos sistemas operacionais vários trabalhos de especificação e verificação destes sistemas
têm sido desenvolvidos.
Entretanto, apesar da diferença temporal existentes em alguns trabalhos, as estraté-
gias utilizadas em cada um possuem como fator comum a simplificação e modularização
dos sistemas desenvolvidos, criando camadas e focando em partes específicas dos sis-
temas. Devido a isso, essa observação serviu como marco inicial para a especificação
desenvolvida nesse trabalho.
Além disso, um trabalho bastante proveitoso no desenvolvimento de uma completa
verificação formal do FreeRTOS é do seL4. Através dele, sabe-se a que a criação de
um novo sistema formalmente verificado é precedida pela verificação formal de um sis-
tema similar. Com isso, essa dissertação pode servir como início da especificação do
29
FreeRTOS, fator importante para o desenvolvimento de um micronúcleo fundamentado
no FreeRTOS.
30
31
3 FREERTOS
O FreeRTOS é um micronúcleo de sistema de tempo real enxuto, simples e de fácil
uso. O seu código fonte, em C com partes em assembly, é aberto e possui um pouco
mais de 2.200 linhas de código, que são essencialmente distribuídas em quatro arquivos:
task.c, queue.c, croutine.c e list.c. Um diferencial desse sistema está na sua portabilidade,
sendo o mesmo oficialmente portável para 17 arquiteturas mono processador diferentes,
entre elas a PIC, ARM e Zilog Z80, as quais são amplamente utilizadas em sistemas
computacionais embutidos (Richard Barry, 2009a).
Como a maioria dos micronúcleos atuais, o FreeRTOS provê, para os seus usuários,
acesso facilitado aos recursos de hardware, agilizando o desenvolvimento de sistemas de
tempo real. Desse modo, ele funciona como na figura 3.1, uma camada de abstração, lo-
calizada entre a aplicação e o hardware, que tem o papel de esconder dos desenvolvedores
de aplicações detalhes do hardware, no qual as aplicações serão implementadas(David
Kalinsky, 2003).
Figura 3.1: Camada abstrata proporcionada pelo FreeRTOS.(Richard Barry, 2009a)
Para prover tal abstração, o FreeRTOS possui um conjunto de bibliotecas de tipos
e funções que devem ser linkeditadas1 com o código da aplicação a ser desenvolvida.
Juntas, essas bibliotecas fornecem aos desenvolvedores serviços como gerenciamento de
tarefa, comunicação e sincronização entre tarefas, gerenciamento de memória e controle
dos dispositivos de entrada e saída(Richard Barry, 2009a).
Devido à sua portabilidade e por ser utilizado em ambientes com limitações de hard-
ware, o FreeRTOS disponibiliza uma biblioteca para uma pré-configuração antes de sua
execução. Essa biblioteca é formada por atributos que armazenam as definições de con-
figuração do usuário. Com isso, as aplicações desenvolvidas com o FreeRTOS podem
tornar-se enxutas e adaptadas, provendo uma melhor utilização dos recursos de hardware.
1Processo que liga o código da aplicação ao código das funcionalidades de outras bibliotecas utilizadas
por ela.
32
Para proporcionar as garantias temporais exigidas pelos STR, o FreeRTOS dispõe
basicamente de três propriedades: escalonador preemptivo baseado na prioridade, tempo
de bloqueio e controle do estouro de tempo. No primeiro, o escalonador dá preferência de
execução para as tarefas mais importantes e compartilha o tempo de processamento entre
as tarefas em execução. No segundo, é atribuído um tempo relacionado ao evento de
bloqueio de uma tarefa. No último, o tempo de execução do sistema é tratado quando este
excede seu limite de armazenamento. Tais propriedades serão comentadas na seção 3.1.3.
A seguir, este capítulo está organizado em seções de acordo com os principais serviços
oferecidos pelo FreeRTOS. A cadaseção encontra-se uma parte comentando as abstrações
de hardware responsável pela implementação do serviço e as funções da API que disponi-
bilizam o mesmo.
3.1 Gerenciamento de tarefas e co-rotinas
Sabe-se que uma aplicação é formada por várias rotinas, responsáveis por realizar as
funcionalidades da aplicação. No FreeRTOS, as unidades responsáveis por abrigar essas
rotinas são as tarefas e as co-rotinas. Nessa seção será demonstrado como esses elementos
funcionam, suas diferenças e unidade de gerenciamento.
3.1.1 Tarefa
Para entender como funciona o gerenciamento de tarefas do FreeRTOS, é necessário
primeiramente entender o conceito de tarefa. Tarefa é uma unidade básica de execução
que compõe os sistemas, os quais, para realizar suas atividades, geralmente possuem
várias tarefas com diferentes obrigações(Richard Barry, 2009a). Para o FreeRTOS, as
principais características de uma tarefa são:
Estado: demonstra a atual situação da tarefa;
Prioridade: indica a importância da tarefa para o sistema, uma prioridade varia de zero
até uma constante máxima pré configurada pelo projetista;
Pilha de execução: local onde uma tarefa armazena informações necessárias para a sua
execução;
Contexto próprio: capacidade de uma tarefa armazenar o ambiente de execução quando
suas atividades são suspensas; e
Tempo de bloqueio: tempo que uma tarefa pode permanecer bloqueada à espera de
algum evento.
Em um sistema, uma tarefa pode assumir vários estados, que variam de acordo com
a sua situação. O FreeRTOS disponibiliza quatro tipos de estados diferentes para uma
tarefa, sendo eles:
Em execução: indica que a tarefa está em execução;
Pronta: indica que a tarefa está pronta para entrar em execução, mas não está sendo
executada;
Bloqueada: indica que a tarefa está esperando por algum evento para continuar a sua
execução; e
33
Suspensa: indica que a tarefa foi temporariamente inativa, por opção do usuário, mas
não aguarda nenhum evento.
Ao entrar no estado bloqueada, a tarefa possui um tempo de bloqueio, relacionado ao
evento que ela aguarda. Este evento pode ser temporal ou estar ligado às outras abstrações
de hardware (fila de mensagens, semáforo e mutex). No evento temporal, o tempo de blo-
queio indica o instante que a tarefa deve retornar do bloqueio e, no evento das abstrações
de hardware, o tempo de bloqueio informa a quantidade de instantes que a tarefa pode
aguardar por esse evento.
Como será visto no decorrer do capítulo, o tempo de bloqueio será informado em
cada funcionalidade capaz de bloquear uma tarefa. Quando uma tarefa atinge seu tempo
de bloqueio sem sair desse estado ela é dita excedente e passa para um estado de controle
interno informando que seu tempo de bloqueio estourou.
No FreeRTOS, uma tarefa só possui um estado em um determinado instante. As
alterações de estado de uma tarefa funcionam como demonstra o diagrama da figura 3.2.
Uma tarefa com o estado em execução pode assumir os estados pronta, bloqueada ou
suspensa. Uma tarefa com o estado pronta pode ser suspensa ou entrar em execução, e as
tarefas com o estado bloqueada ou suspensa só podem ir para o estado pronta.
Figura 3.2: Diagrama de estados de uma tarefa no FreeRTOS.(Richard Barry, 2009a)
Por fim, vale enfatizar que, por tratar-se de um sistema operacional para arquiteturas
mono-processadores, o FreeRTOS não permite que mais de uma tarefa seja executada
ao mesmo tempo. Assim, em um determinado instante, apenas uma das tarefas com
estado pronta pode assumir o processador e entrar no estado em execução. Com isso, para
decidir qual tarefa entrará em execução, o FreeRTOS possui um mecanismo denominado
escalonador, o qual será detalhado na seção 3.1.3.
3.1.1.1 Tarefa ociosa
No FreeRTOS existe uma tarefa especial, denominada Tarefa Ociosa, que é executada,
como o nome sugere, quando o processador encontra-se ocioso, ou seja, quando nenhuma
outra tarefa estiver em execução, ou pronta para entrar em execução. Essa tarefa tem como
principal funcionalidade liberar áreas de memória que não estão sendo mais utilizadas
34
pelo sistema. Por exemplo, quando uma aplicação cria uma nova tarefa, uma área da
memória é reservada a ela. Em seguida, quando essa tarefa é excluída do sistema, a
memória destinada a ela continua ocupada, sendo esta liberada somente quando a tarefa
ociosa entrar em execução. A tarefa ociosa deve possuir prioridade menor do que as
demais tarefas do sistema e, por isso, ela só é executada quando nenhuma outra tarefa
estiver em execução.
3.1.2 Co-rotinas
Outro conceito importante suportado pelo FreeRTOS é o conceito de co-rotinas. As-
sim como as tarefas, co-rotinas são unidades de execução independentes que formam uma
aplicação. Elas também são formadas por uma prioridade e um estado responsáveis, re-
spectivamente, pela importância da co-rotina no sistema e pela situação da mesma. Para
o FreeRTOS, o suporte às co-rotinas é opcional e pré-configurável antes da execução, em
tempo de compilação (Richard Barry, 2009a).
Uma diferença crucial entre co-rotinas e tarefas está no contexto do ambiente de ex-
ecução. Co-rotinas não possuem contexto de execução próprio. Consequentemente, sua
pilha de execução é compartilhada com as demais co-rotinas do sistema, diferente das
tarefas, que possuem uma pilha própria para o armazenamento do seu contexto de exe-
cução.
Devido ao fato de co-rotinas compartilharem a mesma pilha de execução, a utilização
dessa entidade deve ser feita de forma cuidadosa, pois uma informação armazenada por
uma co-rotina pode ser alterada por outra.
Os estados possíveis para uma co-rotina são:
Em execução: indica que uma co-rotina está em execução;
Pronta: indica que uma co-rotina está pronta para ser executada, mas não está em exe-
cução; e
Bloqueada: indica que a co-rotina está bloqueada esperando por algum evento para
continuar a sua execução.
Como as tarefas, co-rotinas possuem somente um estado em um determinado in-
stante, assim, as transições entre os estados de uma co-rotina ocorrem como demonstra a
figura 3.3, onde uma co-rotina em execução pode ir tanto para o estado pronta como para
o estado bloqueada. Uma co-rotina de estado bloqueada só pode ir para o estado pronta
e uma co-rotina de estado pronta só pode ir para o estado em execução. Um detalhe nos
estados das co-rotinas é o estado suspensa, não presente nesse elemento.
Assim como nas tarefas, a decisão de qual co-rotina irá entrar em execução é feita
pelo escalonador, através da chamada a uma funcionalidade específica.Esse processo será
melhor explicado na seção a seguir.
3.1.3 Escalonador de tarefas
O escalonador é a parte mais importante do sistema. Ele é responsável por escolher
qual unidade de execução (tarefa ou co-rotina) irá ocupar o processador, controlar o es-
touro de tempo do sistema e gerenciar o tempo de bloqueio das unidades de execução. No
FreeRTOS, o escalonador pode funcionar de três modos diferentes relacionados ao seu
tipo de interrupção e configuráveis em tempo de compilação. São eles:
35
Figura 3.3: Grafo de estados de uma co-rotina.(Richard Barry, 2009a)
• Preemptivo: Quando o escalonador interrompe a unidade em execução, alterando
assim o seu estado, e ocupa o processador com outra unidade;
• Cooperativo: Quando o escalonador não tem permissão de interromper a unidade
em execução. Assim, a interrupção da execução da unidade em processamento e
a chamada ao escalonador para decidir quem irá entrar em execução devem ser
implementadas pelo projetista; e
• Híbrido: Quando o escalonador pode comportar-se tanto como preemptivo como
cooperativo.
Para as tarefas, o escalonador funciona de forma preemptiva, sendo que a decisão de
qual tarefa deve entrar em execução é baseada na seguinte política de prioridade: a tarefa
em execução deve ter prioridade maior ou igual às tarefas de estado pronta. Dessa forma,
sempre que uma tarefa, com prioridade maior que a tarefa em execução, entrar no estado
pronta, ela deve imediatamente entrar em execução. Um exemplo dessa política pode
ser visto na figura 3.4,onde três tarefas, em ordem crescente de prioridade, disputam a
execução do processador.
Um fato a adicionar sobre a política de funcionamento do escalonador é que, quando
duas ou mais tarefas de estado pronta tiverem prioridades iguais e maiores que as demais
tarefas do mesmo estado, o tempo de execução será divido entre essas tarefas. Com
isso, ao possuir duas tarefas de prioridades máximas no estado pronta, essas tarefas irão
alternadamente ser executadas pelo processador.
Para as co-rotinas, o escalonador funciona de forma cooperativa e baseada na prio-
ridade. A co-rotina em execução é quem decide o momento da sua interrupção e, em
seguida, o sistema deve chamar o escalonador através de uma funcionalidade específica
para decidir qual será a próxima co-rotina a entrar em execução. A escolha da próxima
co rotina a ser executada também é baseada na maior prioridade, assim como ocorre com
as tarefas. Um exemplo do funcionamento do escalonador pode ser visto na seção 3.3.4.
O controle do tempo de execução do sistema é feito pela contagem de instantes que
este iniciou suas atividades. Para isso, uma variável de tipo definido de acordo com
o processador é reservada para armazenar o tempo de execução. Entretanto, todo tipo
de dados possui o seu valor máximo e, quando o tempo de execução atinge esse valor,
ocorreu um estouro de tempo.
O tratamento do estouro de tempo está ligado principalmente às tarefas bloqueadas.
Quando o sistema chega no tempo de bloqueio de uma tarefa, esta deve retornar para o
36
1. Tarefa 1 entra no estado pronta, como não há nenhuma tarefa em execução esta assume
controle do processador entrando em execução.
2. Tarefa 2 entra no estado pronta, como esta tem prioridade maior do que a tarefa 1 ela entra
em execução passando a tarefa 1 para o estado pronta.
3. Tarefa 3 entra no estado pronta, como está tem prioridade maior do que a tarefa 2 ela entra
em execução passando a tarefa 2 para o estado pronta.
4. Tarefa 3 encerra a sua execução, sendo a tarefa 2 escolhida para entrar em execução por ser
a tarefa de maior prioridade no estado pronta.
5. Tarefa 2 encerra a sua execução e o funcionamento do escalonador é passado para a tarefa
1.
Figura 3.4: Funcionamento de um escalonador preemptivo baseado na prioridade.
estado pronta2. Caso isso não ocorra, a tarefa é classificada como excedente de tempo.
No momento do estouro de tempo o escalonador reinicia o tempo de execução do sistema
e retorna as tarefas em excedentes para a lista de tarefas bloqueadas.
3.1.4 Biblioteca
Para disponibilizar as características discutidas nesta seção, o FreeRTOS contém um
conjunto de funcionalidades que podem ser classificados da seguinte forma: criação de
tarefas, controle de tarefas, utilitários de tarefas, controle do escalonador e gerenciamento
de co-rotinas. A seguir, tem-se em detalhes a descrição de cada uma dessas funcionalides.
3.1.4.1 Criação de Tarefas
Essa parte é responsável pela entidade tarefa e sua criação. Nela, estão presentes um
tipo, responsável por representar uma tarefa do sistema, e duas funcionalidades, uma para
a criação e outra para a remoção de tarefas do sistema. Em seguida, tem-se o tipo e as
funcionalidades que compõem a biblioteca em questão.
• xTaskCreate: cria uma nova tarefa para o sistema;
2As tarefas bloqueadas por um evento temporal devem retornar para o estado pronta quando o tempo de
execução é igual ao seu tempo de bloqueio e as bloqueadas por eventos das abstrações de hardware devem
ser desbloqueada até o seu tempo de bloqueio.
37
• vTaskDelete: remove uma tarefa do sistema3; e
• xTaskHandle: tipo pelo qual uma tarefa é referenciada. Por exemplo, quando uma
tarefa é criada através do método xTaskCreate, este retorna uma referência para a
nova tarefa através do tipo xTaskHandle.
3.1.4.2 Controle de tarefas
A parte de controle de tarefas realiza operações sobre as tarefas do sistema. Ela
disponibiliza funcionalidades capazes de bloquear, suspender e reativar uma tarefa do
sistema e informar e alterar a prioridade de uma tarefa no sistema. A lista das principais
funcionalidades pertencentes a essa classificação pode ser vista a seguir:
• vTaskDelay: bloqueia uma tarefa por um determinado tempo. Nessa funcionali-
dade, para calcular o tempo em que a tarefa deve permanecer bloqueada, será levado
em consideração o instante da chamada à funcionalidade. Devido a isso, essa fun-
cionalidade não é recomendada para a criação de tarefas cíclicas, pois o instante em
que ela é chamada pode variar a cada execução da tarefa, por causa das interrupções
que uma tarefa pode sofrer;
• vTaskDelayUntil: bloqueia uma tarefa por um determinado tempo. Essa funcional-
idade, diferente da vTaskDelay, calcula o tempo que a tarefa deve permanecer blo-
queada com base no instante do último desbloqueio da tarefa. Assim, se ocorrer
uma interrupção no momento da chamada à funcionalidade, o instante em que a
tarefa foi desbloqueada não ira mudar. Com isso, esse método torna-se recomendável
para a criação de tarefas cíclicas;
• uxTaskPriorityGet: informa a prioridade de uma determinada tarefa;
• vTaskPrioritySet: muda a prioridade de uma determinada tarefa;
• vTaskSuspend: coloca uma determinada tarefa no estado suspensa;
• vTaskResume: coloca uma determinada tarefa suspensa no estado pronta; e
• xTaskResumeFromISR: funcionalidade usada pelo tratamento de interrupções do
sistema. Ela coloca uma determinada tarefa suspensa para o estado pronta.
3.1.4.3 Utilitários de tarefas
O FreeRTOS disponibiliza para o usuário informações importantes a respeito das tare-
fas e do escalonador de tarefas. Nesta parte da biblioteca, estão presentes funcionalidades
capazes de retornar uma referência para a atual tarefa em execução, retornar o tempo de
funcionamento e estado do escalonador e retornar o número de tarefas que estão sendo
gerenciadas pelo sistema. Uma lista das principais funcionalidades dessa biblioteca é
encontrada a seguir:
• xTaskGetCurrentTaskHandle: retorna uma referência para a atual tarefa em exe-
cução;
3A memória alocada pela tarefa será liberada somente quando a tarefa ociosa entrar em exe-
cução(seção 3.1.1.1).
38
• uxTaskGetStackHighWaterMark: retorna a quantidade de espaço restante na
pilha de uma tarefa;
• xTaskGetTickCount: retorna o tempo decorrido desde a inicialização do escalon-
ador;
• xTaskGetSchedulerState: retorna o estado do escalonador;
• uxTaskGetNumberOfTasks: retorna o número de tarefas do sistema;
• TaskCallApplicationTaskHook: executa a função gancho, função associada a uma
tarefa para preceder a sua execução; e
• TaskSetApplicationTag: associa uma ’tag’ a uma tarefa. Essa ’tag’ será utilizada
principalmente pelas funcionalidades de rastreamento do sistema. Entretanto, é
possível usar essa ’tag’ para associar uma função gancho a uma tarefa. Essa função
é executada através da chamada à funcionalidade TaskCallApplicationTaskHook,
informando a tarefa associada.
3.1.4.4 Controle do Escalonador
Nessa parte estão presentes as funcionalidades responsáveis por controlar as ativi-
dades do escalonador de tarefas. Essas iniciam, finalizam, suspendem e reativam as ativi-
dades do escalonador. Entre elas, as principais são:
• vTaskStartScheduler: inicia as atividades do escalonador, ou seja, inicializa o
sistema;
• vTaskEndScheduler: encerra as atividades do escalonador, ou seja, finaliza o sis-
tema;
• vTaskSuspendAll: suspende as atividades do escalonador
• xTaskResumeAll: reativa o escalonador quando o mesmo está suspenso;
• taskYIELD: força a troca de contexto4 entre tarefas;
• taskENTER_CRITICAL: indica o início de uma região crítica, desabilita tempo-
rariamente a característica de preempção do escalonador impedindo que a tarefa em
execução seja interrompida por outra;
• taskEXIT_CRITICAL: indica o final de uma região crítica, permitindo que ocorra
novamente o escalonamento preemptivo;
• taskDISABLE_INTERRUPTS: Desabilita as interrupções do microcontrolador;
e
• taskENABLE_INTERRUPTS: Habilita as interrupções do microcontrolador.4Troca de contexto é a operação na qual a tarefa em execução é trocada por outra. Para que a troca de
contexto seja realizada, deve existir uma tarefa de prioridade igual à da tarefa em execução.
39
3.1.4.5 Co-rotinas
Por fim, tem-se a parte de gerenciamento de co-rotinas. Nela, estão presentes as fun-
cionalidades e tipos responsáveis por criar e controlar o elemento co-rotina. A lista com-
pleta das funcionalidades presentes nessa biblioteca pode ser vista a seguir:
• xCoRoutineHandle: tipo que representa uma co-rotina.
• xCoRoutineCreate: cria uma nova co-rotina no sistema.
• crDELAY: bloquea uma co-rotina durante uma determinada quantidade de tempo.
• crQUEUE_SEND: envia uma mensagem para uma fila através de uma co-rotina.
• crQUEUE_RECEIVE: recebe uma mensagem de uma fila através de uma co-
rotina.
• crQUEUE_SEND_FROM_ISR: envia uma mensagem para uma fila, através de
uma co-rotina responsável por tratar uma interrupção.
• crQUEUE_RECEIVE_FROM_ISR: recebe uma mensagem de uma fila, através
de uma co-rotina responsável por tratar uma interrupção.
• vCoRoutineSchedule: chama o escalonador para escolher e colocar em execução
a co-rotina de maior prioridade entre as co-rotinas de estado pronto.
3.2 Comunicação e sincronização entre tarefas
Frequentemente tarefas necessitam comunicar-se entre si. Por exemplo, a tarefa A
depende da leitura do teclado, feita pela tarefa B, para disponibilizar em uma tela as
teclas digitadas pelo usuário. Para que essa comunicação possa ser estruturada e sem
interrupções, os sistemas operacionais possuem mecanismos específicos de comunicação.
No FreeRTOS, os mecanismos responsáveis pela comunicação entre as tarefas são
a fila de mensagens, o semáforo e o mutex (Mutual Exclusion). A seguir, tem-se em
detalhes o que são cada um desses mecanismos.
3.2.1 Fila de Mensagens
Filas de mensagens são estruturas primitivas de comunicação entre tarefas. Elas fun-
cionam como túneis, através dos quais tarefas enviam e recebem mensagem (figura 3.5).
Assim, quando uma tarefa necessita comunicar-se com outra, ela envia uma mensagem
para o túnel para que outra tarefa possa ler sua mensagem (Qing Li; Carolyn Yao, 2003).
Figura 3.5: Funcionamento de uma fila de mensagens.
No FreeRTOS, uma fila de mensagens é formada por:
• Lista demensagens: local onde as mensagens enviadas para a fila são armazenadas.
• Lista de tarefas bloqueadas por escrita: lista de tarefas bloqueadas ao tentar
enviar uma mensagem para a fila.
40
• Lista de tarefas bloqueadas por leitura: lista de tarefas bloqueadas ao tentar
retirar ou ler uma mensagem da fila; e
• Tamanho das mensagens: tamanho que deve possuir cada mensagem da fila.
• Tamanho da fila: tamanho máximo da fila, ou seja, quantidade de mensagem que
podem ser armazenada na fila.
O funcionamento de uma fila de mensagens no FreeRTOS ocorre da seguinte forma:
Primeiro a tarefa remetente envia uma mensagem para a fila e, em seguida, a tarefa recep-
tora retira a mensagem da fila. Entretanto, se no momento do envio da mensagem, a fila
estiver cheia, a tarefa remetente é bloqueada e colocada na lista de tarefas bloqueadas por
escrita. O mesmo ocorre quando a tarefa receptora receber uma mensagem de uma fila
vazia, neste caso, a tarefa irá para a fila de tarefas bloqueadas por leitura.
A retirada de uma tarefa das listas de bloqueio é baseada na prioridade. Assim, quando
uma mensagem é extraida de uma fila cheia, a tarefa de maior prioridade da fila de tarefas
bloqueadas por escrita é retirada da lista e retornada para o estado pronto. Do mesmo
modo, quando uma mensagem chega a uma fila vazia, a tarefa de maior prioridade da fila
de tarefas bloqueadas por leitura é retirada da fila e colocada no estado pronta.
No momento de enviar uma mensagem para uma fila, a tarefa deve especificar o tempo
máximo que ela pode permanecer bloqueada, aguardando para enviar a mensagem. As-
sim, ao solicitar uma mensagem de uma fila, uma tarefa deve definir o tempo máximo que
ela pode ficar bloqueada, esperando pela chegada de uma mensagem na fila. As funcio-
nalidades que tornam possíveis essas características serão demonstradas na seção 3.2.4.1.
3.2.2 Semáforo
O semáforo é um mecanismo de sincronização entre tarefas. Funciona como uma
guarda para a tarefa executar uma operação sincronizada ou acessar um recurso com-
partilhado. Desse modo, antes de executar tal ação, a tarefa deve solicitar o semáforo
responsável pela guarda da ação. Caso o semáforo esteja disponível, a tarefa realiza a
ação, caso contrário, a tarefa é bloqueada até que o semáforo seja liberado.
O FreeRTOS disponibiliza dois tipos de semáforos para o usuário, o semáforo binário
e o semáforo com contador. A diferença entre eles está no número de tarefas que podem
reter o semáforo ao mesmo tempo. No semáforo binário é possível apenas uma tarefa
manter o semáforo e no semáforo com contador, existe um número fixo de tarefas (maior
ou igual a um) que podem reter o semáforo.
Para controlar o acesso de várias tarefas, o semáforo com contador possui uma var-
iável denominada contador, cujo valor é definido no momento da criação do semáforo.
O seu funcionamento ocorre como demonstra a figura 3.6. Para cada tarefa que retém o
semáforo, o contador é decrementado e, para cada tarefa que libera o semáforo, o conta-
dor é incrementado. Com isso, o semáforo estará indisponível quando o valor do contador
for igual a zero e seu valor não poderá ultrapassar o número definido inicialmente.
No FreeRTOS, os semáforos são implementados através de uma fila de mensagens
que informa o estado do semáforo através da situação da fila. Assim, quando a fila estiver
vazia, indica que o semáforo não poderá ser retido e, nas demais situações da fila, indica
que o semáforo está liberado.
A representação do semáforo binário é uma fila de tamanho um e a representação do
semáforo com contador é uma fila de tamanho igual à capacidade do seu contador. Vale
41
Figura 3.6: Diagrama de estado do semáforo com contador.
lembrar, que as características das filas de tarefas bloqueadas também são herdadas pelo
semáforo e possuem o mesmo comportamento descrito na seção 3.2.1.
3.2.3 Mutex
Mutex é uma estrutura parecida com o semáforo binário. A única diferença entre os
dois é que o mutex implementa o mecanismo de herança de prioridade, o qual impede
que uma tarefa de maior prioridade fique bloqueada à espera de um mutex (inversão de
prioridade).
Omecanismo de herança de prioridade funciona como demonstra a figura 3.7. Quando
uma tarefa solicita o mutex, ele primeiro verifica se a tarefa solicitante possui prioridade
maior que a tarefa com o semáforo. Caso afirmativo, a tarefa que retém o semáforo tem,
momentaneamente, a sua prioridade elevada, para que assim ela possa realizar as suas
funções sem interrupções e, consequentemente, liberar o semáforo mais rapidamente. Um
detalhe interessante desse elemento é que ele utiliza as mesmas funcionalidades do semá-
foro para reter e liberar o mutex. Essas funcionalidades serão explicadas na seção 3.2.4.2.
3.2.4 Biblioteca
Para disponibilizar as características de comunicação e sincronização entre tarefas, o
FreeRTOS dispõe de um conjunto de funcionalidades e tipos em dois conjuntos: gerenci-
amento de fila de mensagens e semáforo/mutex. Juntos, esses conjuntos possuem vinte e
quatro funcionalidades, das quais as principais serão listadas nas seções seguintes.
3.2.4.1 Gerenciamente de fila de Mensagens
O conjunto de funcionalidades de gerenciamento de uma fila de mensagens é respon-
sável pela criação e utilização da entidade fila de mensagens. Nele estão presentes fun-
cionalidades responsáveis por instanciar e remover uma fila do sistema e funcionalidades
que enviam e recebem mensagens de uma fila do sistema. A seguir, é apresentada a lista
das funcionalidades mais relevantes dessa biblioteca.
• xQueueCreate: cria uma nova fila de mensagens no sistema;
• vQueueDelete: remove uma fila de mensagens do sistema;
42
Figura 3.7: Funcionamento do mecanismo de herançade prioridade.
• xQueueSend: envia uma mensagem para uma fila, sem uma determinada locali-
dade;
• xQueueSendToBack: envia uma mensagem para o final de uma fila;
• xQueueSendToFront: envia uma mensagem para o início de uma fila;
• xQueueReceive: retira uma mensagem de uma fila;
• xQueuePeek: lê uma mensagem de uma fila, sem removê-la;
• xQueueSendFromISR: manda uma mensagem para uma fila, a partir de uma tarefa
de tratamento de interrupção;
• xQueueSendToBackFromISR: manda uma mensagem para o final de uma fila, a
partir de uma tarefa de tratamento de interrupção;
• xQueueSendToFrontFromISR: manda uma mensagem para o início de uma fila,
a partir de uma tarefa de tratamento de interrupção; e
• xQueueReceiveFromISR : lê/retira uma mensagem de uma fila, a partir de uma
tarefa de tratamento de interrupção.
3.2.4.2 Semáforo/Mutex
A parte da API responsável por manipular os semáforos e mutex possui funcionalida-
des que criam e removem semáforos e mutex do sistema, como também funcionalidades
utilizadas para solicitar e liberar um semáforo ou mutex. As principais funcionalidades
desta biblioteca podem ser identificadas a seguir:
• vSemaphoreCreateBinary: cria um semáforo binário;
• vSemaphoreCreateCounting: cria um semáforo com contador;
43
• xSemaphoreCreateMutex: funcionalidade usada para criar um mutex;
• xSemaphoreTake: retém um semáforo ou um mutex;
• xSemaphoreGive: funcionalidade usada para liberar um semáforo ou um mutex
retido; e
• xSemaphoreGiveFromISR: libera um semáforo binário ou com contador, a partir
de uma tarefa de tratamento de interrupção (não deve ser utilizada para mutex).
3.3 Utilização prática dos elementos do FreeRTOS
Para construir uma aplicação de tempo real utilizando o FreeRTOS, o desenvolvedor
deve seguir determinadas restrições impostas pelo sistema. A maioria destas restrições
são parâmetros de configuração e modelos para a criação dos elementos do sistema.
Com o intuito de ajudar o desenvolvedor a criar suas primeiras aplicações, o FreeR-
TOS disponibilizou, junto com seu código fonte, aplicações exemplos classificadas por
plataformas. Desse modo, essas aplicações exemplos podem ser utilizadas como pontos
de partida na criação de novos projetos.
Entretanto, a criação e análise de uma nova aplicação no FreeRTOS é uma atividade
que necessita de maior conhecimento sobre as suas funcionalidades, fugindo do objetivo
desse capítulo. Por isso e para um melhor entendimento das explicações apresentadas
neste capítulo, será demonstrada, nas seções seguintes, de forma didática, exemplos da
utilização das principais entidades aqui discutidas, sendo este adaptações dos exemplos
demonstrados em (Richard Barry, 2009a) e, por isso, servindo como exemplos reais de
criação de um sistema.
3.3.1 Utilização da entidade tarefa
No FreeRTOS, as ações realizadas pelas tarefas são colocadas dentro de rotinas, as
quais devem seguir uma estrutura pré-definida, demonstrada pela figura 3.8. Como na
figura 3.8, uma rotina deve ser formada inicialmente por um cabeçalho com o seu nome
seguido de uma lista de parâmetros e o um código fonte, que realiza as ações das tarefas
dentro de um laço infinito.
1 void func t ionName ( void ∗ vPa r ame t e r s ) {
f o r ( ; ; ) {
3 −− Código de a p l i c a ç ã o da t a r e f a . −−
}
5 }
Figura 3.8: Estrutura da rotina de uma tarefa (Richard Barry, 2009a).
Um exemplo concreto da criação de uma tarefa pode ser visto na figura 3.9. Nela, tem-
se a rotina cyclicalTasks, que utiliza a funcionalidade vTaskDelayUntil (seção 3.1.4.2)
para bloquear a execução da tarefa em intervalos iguais de tempo. Essa funcionalidade
possui como parâmetros, respectivamente, o último tempo em que a tarefa foi reativada
do estado bloqueada e o período que a tarefa deve permanecer bloqueada. Em seguida,
a tarefa é criada no sistema através da funcionalidade xTaskCreate que possui como
parâmetros os seguintes argumentos:
44
cyclicalTasks : ponteiro para a rotina que deve ser executada pela tarefa;
“cyclicalTasks” : nome da tarefa utilizada nos arquivos de log do sistema;
STACK_SIZE : tamanho da pilha de execução da função especificado de acordo com o
número de variáveis declaradas na rotina da função;
pvParameters : lista de valores dos parâmetros de entrada da rotina da função;
TASK_PRIORITY : prioridade da tarefa; e
cyclicalTasksHandle : gancho de retorno da tarefa criada.
1 void c y c l i c a l T a s k s ( void ∗ pvPa r ame t e r s ) {
po r tT i ckType xLastWakeTime ;
3 cons t po r tT i ckType xFrequency = 10 ;
/ / I n i c i a l i z a a v a r i á v e l xLastWakeTime com o tempo a t u a l .
5 xLastWakeTime = xTaskGetTickCount ( ) ;
f o r ( ; ; ) {
7 / / Espera pe l o próximo c i c l o .
vTaskDe l ayUn t i l (&xLastWakeTime , xFrequency ) ;
9 / / Código de ação .
}
11 }
13 xTaskHandle c y c l i c a l T a s k sH a n d l e ;
15 xTaskCrea t e ( c y c l i c a l T a s k , " c y c l i c a l T a s k s " ,STACK_SIZE ,
( void ∗ ) pvPa rame te r s , TASK_PRIORITY,& cy c l i c a l T a s k sH a n d l e ) ;
17
v T a s kS t a r t S c h e d u l e r ( ) ;
Figura 3.9: Aplicação formada por uma tarefa cíclica (Richard Barry, 2009a).
Para finalizar o exemplo da figura 3.9, após ser criada a tarefa, o escalonador do sis-
tema deve ser iniciado e com ele a aplicação. Essa operação é feita pela funcionalidade
vTaskStartScheduler(), localizada no final do código.
3.3.2 Utilização da fila de mensagens
A utilização de uma fila de mensagens é resumidamente demonstrada na aplicação da
figura 3.10. Nela, inicialmente tem-se a estrutura AMessage, que define o tipo da men-
sagem que será utilizada. Em seguida, através do método xQueueCreate, é criada uma fila
de mensagens que será referenciada pela variável xQueue, do tipo xQueueHandle. Para
isso, o método xQueueCreate recebe como parâmetros, respectivamente, a quantidade de
mensagens que a fila pode armazenar e o tamanho das mensagens manuseadas por ela.
Estabelecida a fila de mensagens, é necessário agora definir as tarefas que irão enviar
e receber mensagens da mesma. Na figura 3.10, estão presentes apenas as rotinas de
cada uma dessas tarefas, sendo que a explicação completa de como é criada uma tarefa
foi demonstrada na seção 3.3.1. A seguir, tem-se a explanação sobre cada uma dessas
rotinas.
45
1 s t r u c t AMessage {
portCHAR ucMessageID ;
3 portCHAR ucData [ 2 0 ] ;
} xMessage ;
5
xQueueHandle xQueue ;
7 / / Cr ia uma f i l a com capac idade para 10 p o n t e i r o s
/ / para a e s t r u t u r a a AMessage .
9 xQueue = xQueueCrea te ( 10 , s i z e o f ( s t r u c t AMessage ∗ ) ) ;
/ / Ta r e f a para c r i a r a f i l a e p o s t a r um va l o r .
11 void sendTask ( void ∗ pvPa r ame t e r s ) {
s t r u c t AMessage ∗pxMessage ;
13 i f ( xQueue == 0) {
/ / Falha na c r i a ç ão da f i l a .
15 } e l s e {
/ / Env ia um po n t e i r o para a e s t r u t u r a AMessage .
17 / / Não b l o qu e i a se a f i l a e s t i v e r c h e i a .
pxMessage = &xMessage ;
19 xQueueSend ( xQueue , ( void ∗ ) &pxMessage , ( po r tT i ckType ) 0 ) ;
}
21 / / . . . Re s t o do cód igo da t a r e f a .
}
23
/ / Ta r e f a para r e c e b e r da f i l a .
25 void r e c e i v eT a s k ( void ∗ pvPa r ame t e r s ) {
s t r u c t AMessage ∗pxRxedMessage ;
27 i f ( xQueue !=0 ) {
/ / Recebe a mensagem da f i l a c r i a da . B loque i a por
29 / / 10 t i c k s se um mensagem não e s t i v e r d i s p o n í v e l .
i f ( xQueueReceive ( xQueue ,&( pxRxedMessage ) , ( po r tT i ckType ) 10) ) {
31 / / pcRxedMessage apon ta para a e s t r u t u r a
/ / AMessage v a r i á v e l po s t ada pe l a vATask .
33 }
}
35 / / . . . Re s t o do cód igo .
}
Figura 3.10: Aplicação que utiliza uma fila de mensagens (Richard Barry, 2009a).
Para enviar uma mensagem para a fila xQueue, a rotina sendTask utiliza-se da fun-
cionalidade xQueueSend. Essa funcionalidade possui como parâmetros a fila para qual a
mensagem será enviada, a mensagem que será enviada para a fila e o tempo máximo que
a tarefa poderá ficar bloqueada aguardando