Submitted by Diogo Barreiros (diogo.barreiros@ufba.br) on 2017-02-17T16:37:53Z
No. of bitstreams: 1
barboza2006.pdf: 716139 bytes, checksum: 56397fad812dffadf11ce4841ed6c59c (MD5) / Approved for entry into archive by Vanessa Reis (vanessa.jamile@ufba.br) on 2017-02-21T11:53:04Z (GMT) No. of bitstreams: 1
barboza2006.pdf: 716139 bytes, checksum: 56397fad812dffadf11ce4841ed6c59c (MD5) / Made available in DSpace on 2017-02-21T11:53:04Z (GMT). No. of bitstreams: 1
barboza2006.pdf: 716139 bytes, checksum: 56397fad812dffadf11ce4841ed6c59c (MD5) / 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.
| Identifer | oai:union.ndltd.org:IBICT/oai:192.168.11:11:ri/21586 |
| Date | 26 June 2006 |
| Creators | Barboza, Frederico Jorge Ribeiro |
| Contributors | Andrade, Aline Maria dos Santos, Silva, Flávio Moraes Assis, Lima, George Marconi de Araújo, Costa, Eduard Montgomery Meira, Haeusler, Edward Hermann, Monteiro, José Augusto Suruagy |
| Publisher | Escola Politécnica / Instituto de Matemática, Programa de Pós-Graduação em Mecatrônica, UFBA, brasil |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Source | reponame:Repositório Institucional da UFBA, instname:Universidade Federal da Bahia, instacron:UFBA |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0054 seconds