Detalhes bibliográficos
| Ano de defesa: |
2006 |
| Autor(a) principal: |
Barboza, Frederico Jorge Ribeiro |
| Orientador(a): |
Andrade, Aline Maria dos Santos |
| Banca de defesa: |
Costa, Eduard Montgomery Meira,
Haeusler, Edward Hermann,
Monteiro, José Augusto Suruagy |
| Tipo de documento: |
Dissertação
|
| Tipo de acesso: |
Acesso aberto |
| Idioma: |
por |
| Instituição de defesa: |
Escola Politécnica / Instituto de Matemática
|
| Programa de Pós-Graduação: |
Programa de Pós-Graduação em Mecatrônica
|
| Departamento: |
Não Informado pela instituição
|
| País: |
brasil
|
| Palavras-chave em Português: |
|
| Link de acesso: |
http://repositorio.ufba.br/ri/handle/ri/21586
|
Resumo: |
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. |
