Abstract This paper presents a formal analysis of the device discovery fase of the Bluetooth wireless communication protocol. Prestandan i denna process är resultatet av en komplex interaktion mellan flera enheter, varav några uppvisar slumpmässigt beteende. Vi använder probabilistisk modellkontroll och i synnerhet PRISM-verktyget för att beräkna den bästa och sämsta prestandan för upptäckt av enheter: den förväntade tiden för processen att slutföra och den förväntade strömförbrukningen. Vi illustrerar nyttan av att utföra en uttömmande, lågnivåanalys för att producera exakta resultat i motsats till simuleringsteknik, där ytterligare probabilistiska antaganden måste göras. Vi visar ett exempel på hur till synes ofarliga antaganden kan leda till felaktiga resultatuppskattningar. Vi analyserar också effektiviteten i de förbättringar som gjorts mellan versionerna 1.1 och 1.2 i Bluetooth-specifikationen.
Duflot m.fl. REF presenterar en formell analys av upptäcktsfasen av Bluetooth-protokollet för trådlös kommunikation med hjälp av DTMC-modellen.
A formal analysis of bluetooth device discovery
{'venue': 'International Journal on Software Tools for Technology Transfer', 'journal': 'International Journal on Software Tools for Technology Transfer', 'mag_field_of_study': ['Computer Science']}