Analyzing the procedure for AMP enabled operation in Bluetooth 3.0 using Colored Petri Nets

Bluetooth provides communication between devices via radio frequency in an area of around 10 meters. The Bluetooth specification includes a set of, adopted and fundamental, protocols hierarchically structured. Bluetooth 3.0 is a new version of the technology which is intended to increase the maximum transmission rate provided by the previous versions. Thus an Alternative MAC/PHY (AMP) controller is defined. The AMP operation is activated using the Logical Link Control and Adaptation Protocol (L2CAP). So, in this paper, this procedure is modeled using Colored Petri Nets. The model provides a clear, unambiguous, and precise definition of the AMP enabled operation which is missing in the current specification. The CPN modeling and analysis, using state space technique, has revealed that the existing specification is incomplete. Thus, we propose a more complete specification of the AMP enabled operation, which is also modeled and analyzed using CPNs. The results of the analysis of the modified model show that the new procedure satisfies the behavioral properties of the protocol, such as correct termination.