Naslov
Formal Verification of Logical Link Control and Adaptation Protocol

Autori
Pek, Edgar ; Bogunović, Nikola

Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni

Izvornik
Proceedings of the 12th IEEE Mediterranean Electrotechnical Conference, MELECON 2004 / Matijašević, Maja ; Pejčinović, Branimir ; Tomšić, Željko ; Butković, Željko - Zagreb : Institute of Electrical and Electronics Engineers (IEEE), 2004, 583-586

Skup
12th IEEE Mediterranean Electrotechnical Conference, MELECON 2004

Mjesto i datum
Dubrovnik, Hrvatska, 12.05.2004. - 15.05.2004

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
formal verification ; system design ; distributed systems ; communication protocols

Sažetak
In this paper we have provided formal verification of a configuration process in the Bluetooth logical link control and adaptation protocol (L2CAP). Formal verification has been carried out in a synbolic model checking framework. Hence, NuSMV has been chosen as a tool which enables BDD-based model checking against CTL specifications. Formal description of the protocol is based on an interleaving semantics provided by NuSMV. We have checked important system properties, and described problems related to its specification and verification.

Izvorni jezik
Engleski

Znanstvena područja
Računarstvo

POVEZANOST RADA