PTC29008: Diretrizes para projeto de protocolo
Ainda segundo Gerard Holzmann, no capítulo 2 de seu livro Design and Validation of Computer Protocols, um protocolo possui algumas propriedades desejáveis:
- Simplicidade: um protocolo bem estruturado pode ser construído com um pequeno número de partes bem projetadas e bem entendidas.
- Modularidade: um protocolo que realiza uma função complexa pode ser construído com partes menores que interagem de maneira simples e bem definida. Cada parte menor é um protocolo leve que pode ser desenvolvido separadamente, verificado, implementado e mantido.
- Adequação: um protocolo bem formado não é incompleto, nem possui funções que nunca são de fato utilizadas. Um protocolo bem formado se limita aos recursos existentes, além de ser estável e adaptável.
- Robustez: um protocolo robusto deve funcionar bem em condições normais, e também em situações imprevistas. Ele deve conseguir lidar com cada possível sequência de ações, em todas as possíveis condições. Ele deve ter um projeto mínimo, de forma a remover considerações não essenciais que poderiam impedir sua adaptação a condições não antecipadas.
- Consistência: protocolos não devem apresentar interações que os levem a falhar, tais como deadlocks, livelocks e terminações inesperadas.
A figura a seguir mostra a arquitetura do protocolo de enlace PPP como exemplo de simplicidade e modularidade:
Robustez e consistência são aspectos comportamentais do protocolo, que envolvem portanto a dinâmica de seu funcionamento. O comportamento de um protocolo pode ser descrito de algumas formas, sendo usual utilizar diagramas. A figura a seguir apresenta o comportamento em alto-nível do protocolo PPP (mas não significa que dela se possa concluir que ele seja robusto ou consistente):
Diretrizes de projeto
No mesmo capÍtulo 2 de seu livro, Gerard Holzmann enumera dez regras de projeto de um protocolo:
- Definição do problema: certifique-se de que o problema esteja bem definido, com a identificação de todos os critérios de projeto, requisitos e restrições antes de iniciar um projeto.
- Definição do serviço: deve-se definir o serviço a ser realizado em cada nível de abstração antes de decidir que estruturas devem ser usadas para implementá-los (o que vem antes de como).
- Funcionalidades externas primeiro: projete a funcionalidade externa antes da interna. Primeiro considere a solução como uma caixa-preta e decida como ela interage com seu ambiente. Depois decida como a caixa-preta pode ser organizada internamente. Provavelmente isso consiste de caixas-pretas menores que podem ser refinadas de forma similar.
- Mantenha a simplicidade: protocolos extravagantes são mais propensos a ter bugs que protocolos simples. Eles são mais difíceis de implementar, verificar e comumente menos eficientes. Existem poucos problemas realmente complexos em projetos de protocolos. Problemas que aparentam serem complexos costumam ser problemas misturados. A tarefa dos projetistas é identificar os problemas mais simples, separá-los, e então resolvê-los individualmente.
- Preservar independência: não conectar o que for independente, o que significa separar questões ortogonais.
- Mantenha o projeto extensível: não introduza o que for imaterial. Não restrinja o que for irrelevante. Um bom projeto é facilmente extensível, e resolve uma classe de problemas ao invés de uma única instância.
- Crie um protótipo: antes de implementar um projeto, crie um protótipo de alto-nível, e verifique se os critérios do projeto são atingidos.
- Torne-o eficiente: implemente o projeto, meça seu desempenho e, se necessário, otimize-o.
- Verifique a implementação: confira se a implementação final otimizada é equivalente ao protótipo de alto-nível que foi verificado.
- Não pule as regras 1 a 7
Modelagem do comportamento
Intercâmbios de mensagens entre entidades de um protocolo devem respeitar regras quanto às sequências válidas de mensagens. O conjunto dessas regras é chamado de regras de procedimento (procedure rules).
Um protocolo é um sistema a eventos-discretos. Isso significa que as ações em um protocolo ocorrem em instantes pontuais, e não continuamente. Essas ações, ou acontecimentos, são chamadas de eventos. Por exemplo, a recepção ou envio de uma mensagem, a ocorrência de timeout, o início ou término de uma sessão são eventos ao longo de uma comunicação. Assim, um protocolo interage com seu ambiente (canal de comunicação, usuário), sendo acionado por eventos (ex: recepção de mensagem) que são respondidos com a realização de ações (ex: envio de mensagem). Seu comportamento depende do estado atual do protocolo, o qual é consequência do histórico de eventos passados. Esse tipo de sistema demanda modelos específicos para a descrição das sequências possíveis de eventos, incluindo a informação sobre o estado do protocolo.
Um diagrama de sequência temporal, como mostrado no exemplo do protocolo de bate-papo, apesar de ilustrativo não pode ser usado para especificar as regras de um protocolo. Esse tipo de diagrama é útil para apresentar uma sequência específica de troca de mensagens, mas não todas as sequências possíveis. Quer dizer, ele não tem expressividade para especificar todas as possíveis sequências de mensagens durante as comunicações. Outros tipos de diagramas e métodos formais devem ser usados nesse caso.
Máquinas de Estados Finitos
- Capítulo 8 de Design and Validation of Computer Protocols
- Finite State Machines na Wikipedia
- On Communicating Finite State Machines (artigo seminal)
- Finite State Machines no site Babbage's Bag
- Communicating finite-state machine
- Extended Finite State Machines
Um protocolo de bit-alternado proporciona o envio de mensagens com retransmissão de mensagens perdidas e descarte de mensagens duplicadas. Seu vocabulário é composto pelas mensagens msg0, ack0, msg1, ack1. As regras de procedimento desse protocolo podem ser ilustradas usando diagramas de máquinas de estados finitos, como mostrado a seguir:
Uma máquina de estados finitos (ou simplesmente MEF) é composta de um conjunto de estados (as bolas) e transições (as setas). Um estado representa uma instância de comportamento do sistema (ex: ocioso, espera), e uma transição representa uma mudança de estado. Uma transição possui um estado inicial e um ou mais estados finais, além de uma condição para que ocorra (a isso se chama evento). Esse modelo básico de MEF possui expressividade para modelar alguns sistemas, e apresenta diversas propriedades importantes para analisar o comportamento desses sistemas.
Formalmente, uma MEF é definida pela tupla (Q, q0, S, T), sendo:
- Q: um conjunto não-vazio de estados
- q0: um elemento de Q denominado estado inicial
- S: um conjunto de eventos (ou mensagens), o qual forma um vocabulário
- T: uma relação de transição de estados
A relação de transição de estados T é usualmente representada por uma tabela cujas linhas contêm o estado inicial, uma condição para o disparo da transição, uma ação a ser realizada na transição, e o estado final. No caso da MEF do receptor do protocolo de bit alternado, essa tabela poderia ser:
| Estado inicial | Condição | Ação | Estado final |
|---|---|---|---|
| 0 | ?msg0 | !ack0 | 1 |
| 0 | ?msg1 | !ack1 | 0 |
| 1 | ?msg1 | !ack1 | 0 |
| 1 | ?msg0 | !ack0 | 1 |
O tipo de máquina de estados que se usará em projeto de protocolos é do tipo comunicante. Com ela se podem modelar sistemas concorrentes que interagem por meio de trocas de mensagens. A comunicação entre MEF desse tipo se faz por meio de canais de comunicação e duas primitivas de comunicação: envio e recepção. A notação para o envio e recepção é mostrado a seguir:
- Envio: o envio é indicado por um rótulo de transição (ou evento) no formato nome_de_canal!mensagem. Ex: canal_tx!123 indica o envio da mensagem 123 por meio do canal canal_tx.
- Recepção: a recepção é indicada por um rótulo de transição (ou evento) no formato nome_de_canal?mensagem. Ex: canal_rx?123 indica a recepção da mensagem 123 por meio do canal canal_rx.
Para o projeto do protocolo de comunicação, a MEF tem duas finalidades:
- Modelar as regras de procedimento do protocolo: a MEF torna possível conceber o comportamento do protocolo, definindo o que deve ser feito a depender das mensagens recebidas e transmitidas, entre outros eventos. Além disso, mecanismos internos do protocolo também podem ser modelados com MEF (ex: enquadramento).
- Verificar o comportamento do protocolo: o projeto do protocolo pode esconder problemas sutis e difíceis de identificar. Existem técnicas e ferramentas que auxiliam na verificação da correção das regras de procedimento do protocolo, evidenciando problemas tais como impasses e perdas de sincronismo.
Num primeiro momento, as MEF serão utilizadas para modelar o protocolo de comunicação. Seu uso para verificar a correção do protocolo deve ser realizado após ter sido construído um protótipo.
Atividade
- Modele o aplicativo de rede ping usando MEF comunicante (uma para o lado cliente e outra para o servidor)
- Modele o mecanismo ARQ do tipo pare-espere, considerando comunicações bidirecionais.
- Modele um protocolo de bate-papo P2P usando uma MEF comunicante.
| Descrição do protocolo de bate-papo |
|---|
|
Aplicações de bate-papo (chat) são bastante utilizadas, havendo diversas opções na Internet. Um bate-papo básico, em que se trocam somente mensagens de texto, pode ser implementado sem grande complexidade. Especifique uma aplicação de bate-papo com estas características:
|