**Student: Karl Palmskog ( palmskog@kth.se)**

**Date: May 22, 2006**

Moreover, changes in user behaviour have led to a demand for a more intuitive interface between devices and network-enabled applications. Having session control functions such as ``start'', ``stop'', ``pause'', ``rewind'' and ``fast forward'' can be greatly beneficial for users who regularly experience interruptions in network access -- due to e.g. dynamic behaviour or outages.

One approach to providing delay-, disconnection- and mobility-tolerant communication is to exploit and enhance features which were specified for the session layer in the network protocol stack. Work at Ericsson Research has recently resulted in a description and a proof-of-concept implementation of the Session Management Protocol (SMP), which aims to provide such communication reliability. The thesis project work concerns the formal verification of this protocol.

Currently, the application of formal methods for concurrent programs is not a trivial task and requires knowledge of many fields of computer science, such as automata theory, mathematical logic, proof theory and programming language semantics. But at the same time, there have been progress towards increasing the usability of formal methods and related software tools -- practitioners need no longer be mathematicians.

- Specification of the Session Management Protocol
- Specification of the TCP/IP protocol suite

In light of the complexity of the TCP and SMP state machines and the protocol interactions, it is clear that a formal evaluation of SMP, which focuses on internal consistency and TCP feature interaction, is required. Potential problems include unexpected protocol behaviour leading to ambiguous states or deadlock. Hence, project work includes formally describing and verifying SMP, and thoroughly documenting verification results.

- Understand SMP and TCP behaviour and interaction from specification.
- Provide and motivate choice of formal methods for the verification of SMP.
- Provide a formal description of SMP.
- Provide a formal description of SMP/TCP interaction.
- Apply formal methods for verification of SMP and obtain results. This may be an iterative process, where verification results prompt changes in the formal system description.
- Summarize results, and if necessary, suggest changes to SMP specification.
- Produce a report on the work done.

- Choose a mathematical framework capable of representing concurrent systems.
- Formulate a tool-independent formal description and specification of the protocol.
- Select a software tool incorporating verification algorithms and adapt the model and specification to its format.
- Run the tool using the formal protocol description and specification.
- Evaluate and summarize verification results.

**Analysis of related work**- network mobility approaches and solutions
- TCP/IP and protocol verification
- theories for formal descriptions of concurrent systems
- formal specification of correctness properties
- the feature-interaction problem

Deliverable: thesis Table of Contents with section abstracts, incorporating a literature study report

Deliverable due: June 5, 2006**Choice, and motivation, of formal methods**- selection of mathematical framework
- selection of modeling language
- model-checking algorithms
- specification formalisms
- software tools

Deliverable: thesis chapter section on choice of formal methods and decision procedure

Deliverable due: June 12, 2006**Formal system descriptions**- formal SMP description
- formal description of SMP/TCP interaction
- adaption of formal descriptions to selected software tool

Deliverable: system descriptions

Deliverable due: July 3, 2006

**System specifications**- formulation of formal protocol correctness properties
- adaption of property specifications to selected software tool

Deliverable: system specifications

Deliverable due: July 24, 2006**Verification of systems according to specification**- application of software tool
- reiteration of system descriptions and correctness specification
- error detection and documentation

Deliverable: report on verification results

Deliverable due: September 1, 2006**Summary of results**- evaluation of protocol errors and possible specification changes
- writing thesis

Deliverable: thesis draft

Deliverable due: October 2, 2006

2006-06-08