Behavioral Modeling - WebSocket Protocol

Simplified Web Socket Protocol

Note: this is a contrived example, not the actual protocol.

First, we’d like to express the states of the websocket and the transitions among them. When a websocket is created it starts in the state ready, which we model as the initial state. Upon entering each state initially, the websocket is not accepting any requests. Furthermore, in the states closed and failed, the websocket is not accepting any requests permanently.

The request, if exists, points to either open or close. The children of the request indicate success or failure of the request.

enum Request = open | close
abstract WebSocket
xor states
initial ready
[ initially no request ]
opened
[ initially no request ]
closed --> closed
[ no request ]
failed --> failed
[ no request ]
xor request -> Request ?
success
failure

Example scenarios

The example scenarios serve as test cases, whereby we can state the intended behavior of the websocket. In each case, the constraint must be consistent with the behavior specified above; however, it can be underspecified. For example, the socket can remain in the state opened for an arbitrary number of snapshots until the request to close is received. We express that using the transition -->>. In the other cases, state changes must occur in the next snapshot as required by -->.

Web socket successfully opened and closed

webSocketOpenedClosed : WebSocket

We call such a temporal constraint a trace specification.

Trace 1

Since, the trace specification and the behavior of the websocket are consistent, a trace generator can produce the following trace.

WebSocket11
states
ready
WebSocket12
states
ready
request -> open
success
WebSocket13
states
opened
WebSocket14
states
opened
request -> close
success
WebSocket15
states
closed
WebSocket16
states
closed

Web socket successfully opened but failed to be closed

webSocketOpenedFailed : WebSocket

Trace 2

WebSocket21
states
ready
WebSocket22
states
ready
request -> open
success
WebSocket23
states
opened
WebSocket24
states
opened
request -> close
failure
WebSocket25
states
failed
WebSocket26
states
failed

Web socket failed to be opened

webSocketFailed : WebSocket
[ ready --> request = open && request.failure --> failed --> failed ]

Trace 3

WebSocket31
states
ready
WebSocket32
states
ready
request -> open
failure
WebSocket33
states
failed
WebSocket34
states
failed