• DocumentCode
    3616309
  • Title

    Formal verification of logical link control and adaptation protocol

  • Author

    E. Pek;N. Bogunovic

  • Author_Institution
    Faculty of Electr. Eng. & Comput., Zagreb, Croatia
  • Volume
    2
  • fYear
    2004
  • fDate
    6/26/1905 12:00:00 AM
  • Firstpage
    583
  • 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"
  • Publisher
    ieee
  • Conference_Titel
    Electrotechnical Conference, 2004. MELECON 2004. Proceedings of the 12th IEEE Mediterranean
  • Print_ISBN
    0-7803-8271-4
  • Type

    conf

  • DOI
    10.1109/MELCON.2004.1346997
  • Filename
    1346997
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3616309