| Popis: |
Este trabalho apresenta uma metodologia para representar protocolos TDMA e possíveis falhas que possam ocorrer em sistemas de tempo real tolerantes a falhas utilizando métodos automáticos de verificação. Isto permite garantir diversas propriedades qualitativas e resultados quantitativos como o limite superior de tempo para atingir tais propriedades. Como estudo de caso, apresenta a representação do protocolo TTP/C, determinando o limite de tempo máximo para se atingir a auto-estabilização das visões que cada nodo possui do sistema (Group-membership), possibilitando garantir o tempo máximo de recuperação do sistema, em um cenário de falhas. |
