2. KONTEKST
2.4 L OVVERK OG KRAV
A especificações do FreeRTOS utiliza uma variedade de abstrações de tipos não disponível na AMN como: referências para tarefas, tempo de execução do escalonador e item de uma fila de mensagens. Devido a isso, antes da modelagem do sistema, esses tipos necessi- taram ser especificados, o que é feito pelo módulo Type.
A especificação do módulo Type pode ser vista na figura 6.2. Ela utiliza as estruturas SETSe CONSTANTS para representar os tipos utilizados na especificação. Tipos mais abstratos, como referência de abstrações de hardware, são modelados como conjun- tos abstratos (SETS), e tipos mais concretos, como tempo do escalonador, são especifi- cados como CONSTANTS.
MACHINE Types SETS . . . TASK; ITEM; QUEUE; CONSTANTS . . . QUEUE_NULL, TASK_NULL, PRIORITY , TICK , TICK_INCREMENT , MAX_DELAY , QUEUE_LENGTH , QUEUE_QUANT PROPERTIES . . .
MAX_DELAY ∈ 0..MAXINT ∧
1 ≤ MAX _DELAY ∧
PRIORITY ∈ P(N)∧
TICK ∈ P(N)∧
TICK = 0..MAX _DELAY ∧
TICK_INCREMENT ∈ TICK ∗ TICK → TICK ∧
TICK_INCREMENT = λ(tick, inc).
(tick ∈ TICK ∧ inc ∈ TICK
| (tick + inc)modMAX _DELAY )∧
QUEUE_NULL ∈ QUEUE ∧
TASK_NULL ∈ TASK ∧
QUEUE_LENGTH ∈ P(N)∧
QUEUE_LENGTH = 1..MAXINT ∧
QUEUE_QUANT ∈ P(N)∧
QUEUE_QUANT = 0..MAXINT
END
Figura 6.2: Especificação de tipos do módulo Types.
Os tipos abstratos presentes no módulo da figura 6.2 são: referência para uma tarefa, referência para uma fila de mensagens, referência para um semáforo, referência para um mutex e referência para um item de uma fila de mensagens. As referências para tarefas
são especificadas pelo conjunto TASK , os itens de uma fila de mensagens são modelados por ITEM e as referências para fila de mensagens, semáforo e mutex são todas agrupadas em QUEUE .
Entre os tipos concretos da figura 6.2 estão a prioridade de uma tarefa, PRIORITY , o tempo do escalonador, TICK , o tamanho de uma fila, QUEUE _LENGTH , e a quan- tidade de itens em uma fila, QUEUE _QUANT . O tipo prioridade é informado como subconjunto dos naturais, o tempo do escalonador pode variar de zero a uma constante pré-definida e os tipos para tamanho e quantidade de itens de uma fila são especificados como um conjunto entre zero e o inteiro máximo possível, definido pelo projetista.
Outro detalhe da máquina Types encontra-se nas suas constantes TASK _NULL e QUEUE_NULL e na função TICK _INCREMENT . A constante TASK _NULL repre- senta uma tarefa nula. A constante QUEUE _NULL representa uma fila de mensagens, semáforo ou mutex nulo. Por último, a função TICK _INCREMENT realiza o incre- mento de um valor do tipo TICK obedecendo os limites desse tipo.
O funcionamento da função TICK _INCREMENT é uma soma módulo. Ela soma dois valores de tipo TICK , respeitando os limites definidos pelo tipo. Com isso, ao realizar uma soma cujo resultado é maior que o valor máximo de TICK , o excedente será colocado como resultado da soma. Por exemplo, ao somar 5 com 4, se o limite máximo for 6, o resultado da soma será 3, (5 + 4 mod 6).
6.2.2 Configurações
Para tornar-se portável e mais adaptável, o FreeRTOS disponibiliza um conjunto de configurações que são feitas antes de sua compilação. Basicamente essas configurações informam particularidades da arquitetura alvo e a utilização ou não de determinadas fun- cionalidades do sistema.
Um exemplo de configuração realizada no FreeRTOS pode ser feito quando o sis- tema utiliza a funcionalidade de bloqueio de uma tarefa, xTaskDelay. Para que essa funcionalidade seja linkeditada no sistema desenvolvido, o parâmetro de configuração INCLUDE_vTaskDelaydeve ser configurado como o valor um.
MACHINE FreeRTOSConfig SEES Types CONSTANTS . . . INCLUDE_vTaskPrioritySet, INCLUDE_vTaskSuspend, INCLUDE_uxTaskPriorityGet, INCLUDE_vTaskDelete, INCLUDE_xTaskGetSchedulerState, INCLUDE_xTaskGetCurrentTaskHandle, INCLUDE_vTaskDelay, INCLUDE_vTaskDelayUntil PROPERTIES . . .
INCLUDE_uxTaskPriorityGet ∈ BIT ∧
INCLUDE_vTaskDelete ∈ BIT ∧
INCLUDE_vTaskSuspend ∈ BIT ∧
INCLUDE_xTaskGetSchedulerState ∈ BIT ∧
INCLUDE_vTaskPrioritySet ∈ BIT ∧
INCLUDE_xTaskGetCurrentTaskHandle
∈ BIT ∧
INCLUDE_vTaskDelayUntil ∈ BIT ∧
INCLUDE_vTaskDelay ∈ BIT ∧
END
Figura 6.3: Especificação do módulo FreeRTOSConfig.
Na especificação do FreeRTOSBasic, como demonstra a figura 6.3 os parâmetros de configuração foram todos modelados como CONSTANTS, as quais são delimitadas
pelas PROPERTIES. Assim, a constante INCLUDE_vTaskDelay, que configura a uti- lização da função vTaskDelay, é especificada como um BIT , um tipo concreto especifi- cado na máquina Types que é formado pelos valores zero e um.
6.3 Tarefa
A especificação da entidade tarefa preocupa-se principalmente em modelar os estados de uma tarefa e suas transições. Desse modo, na máquina Task, foram criadas variáveis para representar tais estados e operações responsáveis pela transição e informações sobre o estado de uma tarefa. A explicação completa sobre essa modelagem pode ser vista em seguida.
6.3.1 Estado
Para representar os estados de uma tarefa existem diversas abordagens. A escolhida nessa especificação, devido a sua facilidade com as obrigações de prova, foi os conjuntos. Mais detalhadamente, como demonstra a figura 6.4, o conjunto tasks representa todas as tarefas gerenciadas pelo sistema, o runnable as tarefas habilitadas para a execução, o blocked as tarefas de estado bloqueada, o suspended as tarefas de estado suspensas e a variável running a tarefa de estado em execução. Um detalhe sobre a representação dos estados de uma tarefa está no estado pronto, que é formado pelas tarefas do conjunto runnable menos a tarefa running.
MACHINE Task VARIABLES . . . tasks, blocked , runnable, suspended , running, idle, unblocked INVARIANT . . . tasks∈ FIN(TASK )∧ runnable⊂ tasks∧ blocked⊂ tasks∧ suspended⊂ tasks∧ running∈ TASK ∧ runnable∩ blocked = ∅∧ blocked∩ suspended = ∅∧ suspended∩ runnable = ∅∧
tasks= suspended ∪ blocked ∪ runnable∧
idle∈ TASK ∧
unblocked ⊂ blocked ∧
Figura 6.4: Especificação do estaod de uma tarefa no módulo Task.
Através dos estados da máquina Task da figura 6.4 pode-se perceber algumas re- strições relacionadas ao estado de uma tarefa. Inicialmente a asserção tasks = suspended∪ blocked ∪ runnable garante que não existem tarefas no sistema sem um estado. Em seguida, as asserções runnable ∩ blocked = ∅, blocked ∩ suspended = ∅ e suspended ∩ runnable = ∅ afirmam que não existem tarefas com mais de um estado ao mesmo tempo. Por fim, a expressão running ∈ TASK informa que somente uma tarefa está no estado em execução.
Na especificação da figura 6.4, vale chamar a atenção para a variável idle e o conjunto unblocked que representam, respectivamente, a tarefa ociosa e um conjunto de controle interno, no qual são colocadas as tarefas que devem ser retornadas do estado de bloqueio, explicado melhor na seção 6.4. Assim, no invariante de Task, idle é dita como um ele- mento do conjunto tasks e unblocked como subconjunto do conjunto blocked.
6.3.2 Operações
Após a especificação abstrata da entidade tarefa e seu estado, foram criadas operações para manipular essa característica. Através dessas operações, a transição de estado de uma tarefa pode ser modela. Ao total, foram criadas seis operações, sendo duas responsáveis por gerenciar as tarefas do sistema e quatro responsáveis por manipular seus estados. A lista das operações da máquina Task que gerenciam as tarefas e seus estados pode ser vista a seguir:
t_create : cria uma nova tarefa e adiciona ao conjunto tasks; t_delete : exclui uma tarefa do conjunto tasks;
t_suspend : suspende uma tarefa colocando-a no conjunto suspended; t_resume : retorna uma tarefa do estado suspensa para o estado pronta; t_delayTask : bloqueia uma tarefa colocando-se no conjunto blocked; e
t_removeFromEventList : retira uma tarefa do estado suspensa ou bloqueada e coloca-a no estado pronta.
Nesta seção, serão apresentadas as operações t_create, t_delayTask e t_resume apenas, ficando o leitor convidado a conhecer a especificação das demais funções no repositório do projeto (GALVãO, 2010), no qual encontra-se a especificação completa do FreeRTOS.
6.3.2.1 Operação t _create
A operação responsável por criar uma nova tarefa e coloca-lá no conjunto tasks é demonstrada na figura 6.5. Através dela percebe-se que, utilizando a substituição ANY, uma tarefa que não pertence ao conjunto tasks e não seja a tarefa nula é escolhida e representada por task. Em seguida, essa tarefa é acrescentada em tasks pela substituição tasks := tasks ∪ {task }.
result ←− t_create(priority) = PRE priority ∈ PRIORITY THEN ANY task , n_runnable WHERE task∈ TASK ∧ task�∈ tasks∧ n_runnable ⊂ tasks∧
n_runnable = runnable ∪ {task}∧
task�= TASK _NULL
THEN
tasks:= tasks ∪ {task } �
runnable := n_runnable � CHOICE skip OR running :∈ n_runnable END� result := task END END;
Figura 6.5: Especificação da operação t_create.
Como toda tarefa deve possuir um estado, a tarefa criada na figura 6.5 é inserida no conjunto runnable pelas asserções n_runnable = runnable ∪ {task} e runnable :=
n_runnable . Após isso, esta pode assumir, de forma indeterminada, o estado pronta ou em execução, o que é especificado pela substituição CHOICE e a asserção running :∈ n_runnable. Dessa forma, se a tarefa criada for a escolhida na atribuição running :∈ n_runnable, ela entrará em execução, caso contrário, ficará no estado pronta. Vale co- mentar que, apesar dessa operação receber uma prioridade como argumento, este só será utilizado no refinamento da mesma.
6.3.2.2 Operação t _delayTask
Para colocar uma tarefa no estado bloqueada, a máquina Task utiliza a operação t_delayTask, exibida na figura 6.6. Esta recebe como parâmetros o tempo que a tarefa deve permanecer bloqueada, tick (o qual será usado apenas nos refinamentos), e a tarefa em execução, task. Enfim, na pré-condição da operação, é informado que a tarefa que será bloqueada não pode ser a tarefa ociosa, running �= idle.
t_delayTask(ticks, task) = PRE task ∈ TASK ∧ task = running∧ running ∈ runnable∧ running �= idle∧ ticks ∈ TICK THEN ANY n_runnable WHERE n_runnable ⊂ tasks∧
n_runnable = runnable − {running}
THEN
runnable := n_runnable �
running:∈ n_runnable
END�
blocked := blocked ∪ {running} END;
Figura 6.6: Especificação da operação t_delayTask.
No corpo da operação t_delayTask da figura 6.5, tem-se o bloqueio da tarefa em execução. Inicialmente, essa tarefa é retirada do conjunto de tarefas habilitadas para entrar em execução através das asserções n_runnable = runnable − {running} e runnable := n_runnable. Em seguida, a atribuição indeterminada running :∈ n_runnable escolhe uma nova tarefa para entrar em execução. Finalmente, a antiga tarefa em execução é colocada no estado bloqueada em blocked := blocked ∪ {running}.
Vale enfatizar que, na operação da figura 6.5, as atribuições são realizadas paralela- mente, o que impede o bloqueio da nova tarefa em execução no lugar da antiga. Pode parecer estranho também receber como parâmetro a tarefa em execução, mas essa decisão foi tomada para facilitar as obrigações de prova do módulo que utiliza tal operação. 6.3.2.3 Operação t _resume
Na operação t_resume da figura, uma tarefa é retirada do estado suspenso e colo- cado no estado pronta. Essa operação recebe como parâmetro a tarefa que retornará do estado pronta, rtask, sendo necessária essa tarefa estar previamente suspensa, o que é especificado em rtask ∈ suspended.
O retorno de uma tarefa do estado suspensa na figura 6.7 é feito da seguinte forma. A tarefa desejada é adicionada no conjunto de tarefa aptas para a execução, n_runnable = runnable∪{rtask } e runnable := n_runnable e, em paralelo, essa é retirada do conjunto de tarefa suspensas, suspended := suspended − {rtask}.
Ao colocar a tarefa rtask da figura 6.7 no conjunto de tarefas habilitadas para serem executadas, esta pode assumir o estado de pronta ou em execução. Tal escolha é feita
t_resume(rtask) = PRE rtask ∈ TASK ∧ rtask ∈ suspended ∧ active= TRUE THEN ANY n_runnable WHERE n_runnable ⊂ tasks∧
n_runnable = runnable ∪ {rtask} THEN runnable := n_runnable � CHOICE running:∈ n_runnable OR skip END END�
suspended := suspended − {rtask } END;
Figura 6.7: Especificação da operação t_resume.
através da atribuição running :∈ n_runnable. Assim, se a tarefa escolhida pela atribuição for rtask, ela irá para o estado em execução e a tarefa em execução para o estado pronta. Caso contrário, rtask assumirá o estado pronta.
6.4 Escalonador
Devido ao escalonador estar relacionado principalmente ao elemento tarefa, a sua especificação também foi feita na máquina Task. Nesta, preocupou-se em especificar principalmente o tempo de execução e a troca de estado das tarefas bloqueadas. A seguir tem-se em detalhes como estas propriedades foram especificadas.
6.4.1 Estado
A parte do estado da máquina Task responsável pelas propriedades do escalonador é demonstrada na figura 6.8. Nela, as variáveis tickCount e tickMissed são representações do tempo de execução do escalonador e a variável active informa o estado do escalonador.
MACHINE Task VARIABLES tickCount , tickMissed , active, INVARIANT active∈ BOOL∧ tickCount∈ TICK ∧ tickMissed ∈ TICK ∧ (active = TRUE ⇒ idle∈ runnable∧ runnable�= ∅∧
TASK_NULL �∈ tasks)
running∈ runnable∧
Figura 6.8: Especifacação da parte do estado da máquina relacionada ao Task. Especificamente, as variáveis da figura 6.8 funcionam da seguinte maneira. Quando o escalonador estiver ativado, active terá o valor TRUE , caso este esteja suspenso o valor será FALSE . É importante comentar que o escalonador pode estar inicializado, mas temporariamente suspenso. Assim o período de inicialização deste é armazenado na variável tickCount e o seu tempo de suspensão é contado em tickMissed, o qual será melhor explicado na seção 6.4.2.3.
deve estar em execução ou pronta e sempre deve existir uma tarefa em execução são especificadas nas asserções idle ∈ runnable e runnable �= ∅. Na continuação, para detalhes internos, foi dito que a tarefa nula não deve fazer parte do sistema e que running deve pertencer ao conjunto de tarefas habilitadas runnable.
6.4.2 Operações
As operações da máquina Task responsáveis pelas características do escalonador são classificadas como operações de consulta e operações de controle. As operações de con- trole realizam mudanças dos estados especificados da máquina Task e as de consulta disponibilizam informações sobre o escalonador. Em seguida, encontra-se a lista dessas operações, sendo as duas primeiras de consulta e as demais de controle:
t_getCurrent : informa a tarefa em execução;
t_getNumberOfTasks : informa o número de tarefas do sistema; t_yield : realiza a escolha da tarefa que deve entrar em execução; t_startScheduler : inicializa o escalonador;
t_endScheduler : encerra o escanolador;
t_incrementTick : executa rotinas do escalonador a cada ciclo de tempo; t_suspendAll : coloca o escalonador no estado suspenso;
t_resumeAll : retorna do estodo bloqueada um conjunto de tarefas; e
t_beforeResumeAll : executa rotinas feitas quando o escalonador é retornado do estado suspenso.
Dentre as operações do escalonador, as mais proveitosas para esta seção são: t_yield, t_startScheduler, t_incrementTick, t_resumeAll e t_beforeResumeAll, as quais serão demonstradas em seguida.
6.4.2.1 t _yield
Para solicitar ao escalonador que verifique se a tarefa em execução deve ser trocada ou não, a máquina Task disponibiliza a operações t_yield da figura 6.9. Nela, a decisão sobre a tarefa em execução é feita de forma não determinística pela atribuição running :∈ runnable. Em refinamentos da especificação, mostrados no capítulo 7, tal decisão será especificada de forma mais concreta.
t_yield = PRE active= TRUE THEN running:∈ runnable END;
Essa mesma ação, descrita no parágrafo anterior deve ser realizada a cada alteração no conjunto de tarefas habilitadas para a execução, runnable. Por isso, nas operações das figuras 6.5, 6.6 e 6.7, a escolha da tarefa em execução é feita de modo similar ao da figura 6.9.
6.4.2.2 t _startScheduler
Uma operação um pouco mais complexa que a t_yield é a t_startScheduler, respon- sável por inicializar as atividades do escalonador, como demonstra a figura 6.10. Nela inicialmente o estado do escalonador é mudado para ativo; em seguida, a tarefa ociosa é criada na variável idle_task. Após isso, esta é adicionada ao conjunto de tarefas do sistema, tasks. Por fim, a tarefa é adicionada ao conjunto de tarefas habilitadas para entrar em execução, o que provoca uma nova escolha da tarefa em execução, feita em running :∈ n_runnable. t_startScheduler = PRE active= FALSE THEN active:= TRUE � ANY idle_task, n_runnable WHERE idle_task ∈ TASK ∧ idle_task �∈ tasks∧ n_runnable ⊂ tasks∧
n_runnable = runnable ∪ {idle_task}
THEN
idle:= idle_task �
tasks:= tasks ∪ {idle_task } �
runnable := n_runnable �
running:∈ n_runnable
END END;
Figura 6.10: Operação t_startScheduler.
6.4.2.3 t _incrementTick
No FreeRTOS, a cada tempo de sistema (interrupção de relógio) o escalonador realiza rotinas. Essas rotinas podem ser resumidas da seguinte forma: Quando o escalonador estiver ativo, ele deve primeiramente incrementar o tempo de execução. Em seguida, este verifica, na lista de tarefas bloqueadas, as tarefas que estão em seu tempo de retorno do bloqueio e as que excederam este tempo. Caso o escalonador esteja suspenso, o seu tempo de suspensão é contabilizado.
Para ajudar a especificar as ações descritas anteriormente, a máquina Task possui a operação t_incrementTick. Nesta são feitas as ações de contagem de tempo e verificação das tarefas que devem retornar do bloqueio. A parte que retorna as tarefas do bloqueio será especificada pela operação t_resumeAll e a verificação das tarefas com o tempo excedente é especificada em futuros refinamentos.
A especificação da operação t_incrementTick pode ser vista na figura 6.11. Inicial- mente, através da substituição IF ela verifica se o escalonador está ativo ou suspenso. Caso ele esteja ativo, o seu tempo é incrementado e uma lista de tarefas, escolhida de forma indeterminada pela substituição ANY, é marcada para o desbloqueio. Caso esse esteja suspenso, o seu tempo de suspensão é contabilizado.
t_incrementTick = BEGIN
IFactive= TRUE THEN
tickCount := TICK _INCREMENT (tickCount, 1) �
ANY n_unblocked WHERE n_unblocked ∈ FIN(TASK )∧ n_unblocked ⊂ blocked THEN unblocked := n_unblocked END ELSE
tickMissed := TICK _INCREMENT (tickMissed , 1)
END END;
Figura 6.11: Operação t_incrementTick. 6.4.2.4 t _resumeAll
A função t_resumeAll tem como objetivo realizar o desbloqueio de um conjunto de tarefas. Essa operação servirá de suporte tanto para as rotinas temporais do escalonador como para as rotinas realizadas no retorna da suspensão deste.
t_resumeAll(tunblocked) = PRE tunblocked ∈ FIN(TASK )∧ tunblocked ⊂ blocked ∧ tunblocked = unblocked THEN IFtunblocked �= ∅ THEN ANY n_runnable WHERE n_runnable ⊂ tasks∧
n_runnable = runnable ∪ tunblocked
THEN runnable:= n_runnable � CHOICE running:∈ n_runnable OR skip END END�
blocked := blocked − tunblocked � unblocked := ∅
END END;
Figura 6.12: Operação t_resumeAll.
Para cumprir o seu objetivo, t_resumeAll foi especificado conforme a figura 6.12. Primeiramente, o conjunto de tarefas que serão retornadas do bloqueio é acrescentado ao conjunto de tarefas habilitadas através das asserções n_runnable := runnable ∪ tunblocked e runnable := n_runnable. Em seguida, através da substituição CHOICE, a escolha da tarefa em execução pode ser feita ou não. Ao final, as tarefas em questão são retiradas do conjunto de tarefas bloqueadas em blocked := blocked − tunblocked e o conjunto de tarefas que devem sair do bloqueio é zerado em unblocked := ∅.
6.4.2.5 t _beforeResumeAll
Por fim, a escolha de quais tarefas serão desbloqueadas no retorno da suspensão do escalonador é feita na operação t_beforeResumeAll. Inicialmente, essa operação atualiza o tempo do escalonador com o tempo que este permaneceu suspenso e em seguida ela ver-
ifica na lista de tarefas bloqueadas as que deveriam sair do bloqueio durante a suspensão do escalonador. Assim, na especificação dessa operação da figura 6.12, a atualização do tempo é feita na asserção tickCount := TICK _INCREMENT (tickCount, tickMissed) e a verificação das tarefas que serão retornadas do bloqueio é feita de forma abstrata pelo substituição ANY. A verificação mais detalhada sobre as tarefas que devem ser retor- nadas é feita no refinamento da operação na seção 7.3.2.3.
t_beforeResumeAll = PRE
active= FALSE
THEN
tickCount := TICK _INCREMENT (tickCount, tickMissed ) �
tickMissed := 0 � ANY n_unblocked WHERE n_unblocked ∈ FIN(TASK )∧ n_unblocked ⊂ blocked THEN unblocked := n_unblocked END END
Figura 6.13: Operação t_resumeAll.
6.5 Fila de mensagens
A abstração de hardware fila de mensagens é um tipo de comunicação entre tarefas através de mensagens que são enviadas e retiradas da fila. Nessa modelagem, uma fila de mensagens é formada por conjuntos de tarefas bloqueadas pela fila e um conjunto de mensagens enviadas para a fila. Para especificar essa característica, a máquina Queue possui um conjunto de estados e para controlar esses estados uma variedade de operações da máquina foi criada. A seguir, é mostrada como esta especificação foi realizada. 6.5.1 Estado
Assim como ocorreu com o elemento tarefa, a especificação das propriedades rela- cionadas a uma fila de mensagens foi feita através de conjuntos, como demonstra a figura 6.14. Inicialmente, o conjunto das filas gerenciadas pelo sistema, queue_msg, é criado. Em seguida, os conjuntos de fila cheia e fila vazia são respectivamente especifica- dos em queues_msg_full e queues_msg_empty. Por fim, a fila de mensagens é associada a um conjunto de itens em queue_items, um conjunto de tarefas bloqueadas por leitura em queue_receiving e um conjunto de tarefas bloqueadas por escrita, em queue_sending. Para entender melhor a especificação dos estados da figura 6.14 é necessário saber primeiramente o significado do conjunto queues. Esse conjunto representa a união de todas as filas de mensagens, semáforos e mutex. Assim queues é criado como uma gen- eralização que agrupa características semelhantes desses três elementos. Tais caracterís- ticas são os conjuntos de tarefas bloqueadas pelos elementos de queues, o que é especifi- cado respectivamente em queue_receiving ∈ QUEUE →+ P(TASK ) e queue_sending ∈ QUEUE→+ P(TASK ).
MACHINE Queue VARIABLES queues, queues_msg, queues_msg_full, queues_msg_empty, queue_items, queue_receiving, queue_sending, first_sending, first_receiving INVARIANT queues ∈ P(QUEUE )∧ queue_receiving ∈ QUEUE →+ P(TASK )∧ queue_sending ∈ QUEUE →+ P(TASK )∧ queues = dom(queue_receiving)∧ queues = dom(queue_sending)∧ queues_msg ⊂ queues∧ queues_msg_full ⊂ queues_msg∧ queues_msg_empty ⊂ queues_msg∧ queue_items ∈ QUEUE →+ P(ITEM )∧ queues_msg = dom(queue_items) first_receiving ∈ QUEUE →+ TASK ∧