| Revista: | Computación y sistemas |
| Base de datos: | PERIÓDICA |
| Número de sistema: | 000360503 |
| ISSN: | 1405-5546 |
| Autores: | Villapol, María Elena1 |
| Instituciones: | 1Universidad Central de Venezuela, Escuela de Ciencias de la Computación, Caracas, Distrito Federal. Venezuela |
| Año: | 2012 |
| Periodo: | Oct-Dic |
| Volumen: | 16 |
| Número: | 4 |
| Paginación: | 423-446 |
| País: | México |
| Idioma: | Inglés |
| Tipo de documento: | Artículo |
| Enfoque: | Analítico, descriptivo |
| Resumen en español | Bluetooth permite la comunicación entre dispositivos a través de frecuencias de radio en un área de alrededor de 10 metros. La especificación Bluetooth incluye un conjunto de protocolos fundamentales y adoptados. El protocolo Bandabase es un protocolo fundamental que es responsable del establecimiento de la conexión entre un maestro y hasta siete dispositivos esclavos. Este artículo describe un modelo del protocolo de establecimiento de conexión y presenta el enfoque del análisis y los resultados. El protocolo es modelado utilizando las Redes de Petri Coloreadas. El modelo proporciona una definición clara, inequívoca y precisa de las acciones consideradas del protocolo de Bandabase, que faltan en la especificación del protocolo actual. El modelo es analizado en función de un conjunto de propiedades generales, tales como la terminación correcta, y un conjunto de propiedades específicas del protocolo Bandabase que se definen en este documento. Algunas de las propiedades se comprueban examinando el grafo de ocurrencia, y las otras se verifican mediante una lógica temporal basada en CTL. Los resultados muestran que el modelo de Bandabase satisface las propiedades definidas |
| Resumen en inglés | Bluetooth provides communication between devices via radio frequency with a range of around 10 meters. The Bluetooth specification includes a set of adopted and fundamental protocols. Baseband is a fundamental protocol that is responsible for the connection establishment among a master and up to seven slave devices. This paper describes a model of the Baseband connection establishment protocol and presents the analysis approach and results. The protocol is modeled using Colored Petri Nets. The model provides a clear, unambiguous and precise definition of the considered features of the baseband protocol, which is missing in the current protocol specification. The model is analyzed for a set of general properties, such as correct termination, and a set of Baseband protocol's specific properties defined in this paper. Some of the properties are checked by querying the occurrence graph, and the others are verified using a CTL-like temporal logic. The results show that the Baseband model satisfies the defined properties |
| Disciplinas: | Ciencias de la computación, Ingeniería |
| Palabras clave: | Redes, Ingeniería de telecomunicaciones, Bluetooth, Logica temporal, Verificación, Redes de Petri |
| Keyword: | Computer science, Engineering, Networks, Telecommunications engineering, Bluetooth, Temporal logic, Verification, Petri nets |
| Texto completo: | Texto completo (Ver HTML) |
