|
[DKNP04]
Marie Duflot, Marta Kwiatkowska, Gethin Norman and David Parker.
A Formal Analysis of Bluetooth Device Discovery.
In T. Margaria and B. Steffen, A. Philippou and M. Reitenspiess (editors), Proc. 1st International Symposium on Leveraging Applications of Formal Methods (ISOLA'04), volume TR-2004-6 of Technical Report, pages 268-275, Department of Computer Science, University of Cyprus.
November 2004.
[ps.gz]
[pdf]
[bib]
[Analyses device discovery in Bluetooth using PRISM.]
|
|
Downloads:
 ps.gz (111 KB)
 pdf (251 KB)
 bib
|
|
Notes:
A journal version of this paper is available as [DKNP06].
A slightly extended version of this paper can also be found here
(deliverable D6).
For further details of this case study, see
this web page.
|
|
Links:
[Google]
[Google Scholar]
|
|
Abstract.
This paper presents a formal analysis of the device discovery phase
of the Bluetooth wireless communication protocol.
The performance of this process is the result of a complex interaction between several devices,
some of which exhibit random behaviour.
We use probabilistic model checking and, in particular, the tool PRISM
to compute the best and worst case expected time for device discovery.
We illustrate the utility of performing an exhaustive, low-level analysis to
produce exact results in contrast to simulation techniques,
where additional probabilistic assumptions must be made.
We demonstrate an example of how seemingly innocuous assumptions
can lead to incorrect performance estimations.
We also analyse the effectiveness of improvements made
between versions 1.1 and 1.2 of the Bluetooth specification.
|