Procedural design — registration and session establishment as state machines

From Sequence Diagram to State Machine

TS 23.502 describes 5G procedures as sequence diagrams — UE sends RegistrationRequest, AMF queries AUSF, AUSF requests challenge, UE responds, AMF queries UDM, and so on. Implementing such a procedure correctly in code requires translating the sequence into a finite state machine. Each "while waiting for X" interval becomes a state. Each message arrival or timer expiry becomes a transition. Each transition has a guard (is this the message we expect from this peer?) and an action (update state, send next message, start timer). The resulting state machine is verifiable: you can enumerate all…