View article

The Session Management Protocol (SMP) is an important part of a session layer for mobile, disconnection-and delay-tolerant communication developed at Ericsson Research. This layer lets applications use sessions instead of sockets to communicate with network endpoints. Such sessions are very persistent, surviving even network outages and changes in network attachment. SMP may run on top of TCP/IP or other network protocols, and handles data integrity and resumption after disconnection and suspension for sessions. It also deals with sending and processing messages related to the communication context.

In this thesis, we formally describe SMP, specify its correctness, and verify several protocol models in the validation language Promela by using the model checker Spin. As a preparation for verification, the protocol is characterized informally in a structured manner. After outlining the modelling and verification approach, we give reports on model checking. In particular, we highlight the detection of an error in data integrity management, and describe how this discovery led to changes in the protocol. By applying abstraction and separating the concerns of safety and liveness, protocol model complexity was reduced to permit exhaustive verification in Spin. Model checking results prompt the conclusion that SMP reliability has increased through the verification effort.