Analysis of the Properties of the Bluetooth Baseband Connection Establishment Using Colored Petri Nets

Fuente: Redalyc
Gespeichert in:
Bibliographische Detailangaben
1. Verfasser: María Elena Villapol
Format: Artículo científico
Sprache:en
Veröffentlicht: Instituto Politécnico Nacional 2012
Schlagworte:
Online-Zugang:
Tags: Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
_version_ 1876470918973227008
author María Elena Villapol
author_facet María Elena Villapol
contents Analysis of the Properties of the Bluetooth Baseband Connection Establishment Using Colored Petri Nets María Elena Villapol Computación Bluetooth verification temporal logic occurrence graph Colored Petri Nets 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. 2012 artículo científico 1405-5546 https://www.redalyc.org/articulo.oa?id=61524670006 en http://www.redalyc.org/revista.oa?id=615 Computación y Sistemas application/pdf Instituto Politécnico Nacional Computación y Sistemas (México) Num.4 Vol.16
format Artículo científico
id redalyc_61524670006
institution Redalyc
language en
publishDate 2012
publisher Instituto Politécnico Nacional
spellingShingle Analysis of the Properties of the Bluetooth Baseband Connection Establishment Using Colored Petri Nets
María Elena Villapol
Computación
Bluetooth
verification
temporal logic
occurrence graph
Colored Petri Nets
Analysis of the Properties of the Bluetooth Baseband Connection Establishment Using Colored Petri Nets María Elena Villapol Computación Bluetooth verification temporal logic occurrence graph Colored Petri Nets 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. 2012 artículo científico 1405-5546 https://www.redalyc.org/articulo.oa?id=61524670006 en http://www.redalyc.org/revista.oa?id=615 Computación y Sistemas application/pdf Instituto Politécnico Nacional Computación y Sistemas (México) Num.4 Vol.16
title Analysis of the Properties of the Bluetooth Baseband Connection Establishment Using Colored Petri Nets
topic Computación
Bluetooth
verification
temporal logic
occurrence graph
Colored Petri Nets
url https://www.redalyc.org/articulo.oa?id=61524670006