Title :
Formal verification of logical link control and adaptation protocol
Author :
E. Pek;N. Bogunovic
Author_Institution :
Faculty of Electr. Eng. & Comput., Zagreb, Croatia
fDate :
6/26/1905 12:00:00 AM
Abstract :
In this paper, we provide a formal verification of a configuration process in the Bluetooth logical link control and adaptation protocol (L2CAP). Formal verification has been carried out in a symbolic model checking framework. Hence, NuSMV has been chosen as a tool which enables the BDD-based model checking against CTL specifications. Formal description of the protocol is based on an interleaving semantics provided by the NuSMV. We checked the important system properties and described the problems related to its specification and verification.
Keywords :
"Formal verification","Protocols","Data structures","Boolean functions","Bluetooth","Interleaved codes","Logic","Safety","Embedded system","Communication system control"
Conference_Titel :
Electrotechnical Conference, 2004. MELECON 2004. Proceedings of the 12th IEEE Mediterranean
Print_ISBN :
0-7803-8271-4
DOI :
10.1109/MELCON.2004.1346997
