Revision 4ad21fff0ec17541eefe44fb8c2639b668923ddb (click the page title to view the current version)

Behavioral Modeling - WebSocket Protocol

Simplified Web Socket Protocol

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

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

Example scenarios

Web socket successfully opened and closed

webSocketOpenedClosed : WebSocket
[ ready --> request = open && request.success --> opened -->> request = close && request.success --> closed --> closed ]

Trace 1

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

Web socket successfully opened but failed to be closed

webSocketOpenedFailed : WebSocket
[ ready --> request = open && request.success --> opened -->> request = close && request.failure --> failed --> failed ]

Trace 2

WebSocket21
states
ready
WebSocket22
request -> open
success
states
ready
WebSocket23
states
opened
WebSocket24
request -> close
failure
states
opened
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
request -> open
failure
states
ready
WebSocket33
states
failed
WebSocket34
states
failed