Insights into States of LE Credit-Based Channel in L2CAP

[tkhang1999]

Hi,

We are currently working on the formal verification of the state machine in L2CAP. As part of this effort, we have been studying the Bluetooth Core Specification 5.4, particularly Vol 3, Part A, Section 6, which specifies the L2CAP state machine. However, this section describes the state machine for the classic channel only.

We are attempting to formalize the state machine for the Low Energy (LE) credit-based channel but have been unable to locate detailed specifications for this in the document. While looking over your implementation of L2CAP, we noticed the defined states for the LeCreditBasedChannel. We are curious about the documentation/references/specifications you used to derive these states. Could you share insights or resources that guided your implementation?

...
class LeCreditBasedChannel(EventEmitter):
    """
    LE Credit-based Connection Oriented Channel
    """
    class State(enum.IntEnum):
        INIT = 0
        CONNECTED = 1
        CONNECTING = 2
        DISCONNECTING = 3
        DISCONNECTED = 4
        CONNECTION_ERROR = 5
...

Ref: https://github.com/google/bumble/blob/main/bumble/l2cap.py#L1048-L1053

[tkhang1999]

@zxzxwu Sorry for tagging you directly! I saw that you recently worked on the L2CAP implementation so I would appreciate it if you could help provide some insights here. Thank you in advance!

[barbibulle]

You're right, the BT spec does not specify a particular set of states for LE credit based channels. Only the request/response signaling messages are defined.
The states in the Bumble implementation are just what I found convenient to represent the states and the transitions between them based on received/sent messages.
Different implementations of the spec may chose an entirely different approach, with or without a state machine, and with possibly different choices for states, if any.