VERIFICAÇÃO FORMAL DA FUNÇÃO DE CONTROLE DE ACESSO AO MEIO DO PROTOCOLO IEEE 802.11 E INVESTIGAÇÃO DA SUA APLICABILIDADE EM SISTEMAS DE TEMPO-REAL

Abstract

O termo IEEE 802.11 diz respeito a uma família de especificações que buscam obter conectividade sem fio para estações fixas, portáveis e móveis em uma rede local. Redes IEEE 802.11 têm, recentemente, despertado interesse como tecnologia de suporte para a comunicação em aplicações sem fio na automação, em particular em aplicações de chão de fábrica e de controle de plantas, onde, muitas vezes, requisitos de tempo-real e requisitos de confiabilidade são necessários. Neste contexto, o uso de métodos formais permite a obtenção de um conhecimento mais preciso sobre as propriedades do protocolo bem como a especificação e verificação destas propriedades. Este trabalho apresenta uma especificação e verificação formal da função de controle de acesso ao meio da sub-camada MAC do padrão IEEE 802.11 usando UPPAAL, um verificador de modelos gratuito, que suporta os conceitos de relógios e tempo. O uso do UPPAAL permitiu considerar, dentro da modelagem, as características temporais do protocolo. A verificação procurou identificar uma série de propriedades que fornecesse aos projetistas de aplicações e sistemas de tempo-real um conjunto mínimo de garantias relativas aos canais de comunicação. Entre as propriedades verificadas, destacamos a habilidade das estações possuírem acesso ao meio dentro de um tempo finito e conhecido e, portanto, a adequação do protocolo como suporte a aplicações que necessitem de garantias temporais.