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

Abstract

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.