A forum for Spin users
You are not logged in.
Pages: 1
Thanks, I'd be interested by any pointer. I know the work done by Cambridge http://www.cl.cam.ac.uk/~pes20/Netsem
but this is much more detailed than what I'd be able to do
Hello,
The Transmission Control Protocol (TCP) is widely used in the Internet. TCP extensions are frequently proposed to improve TCP or its performance. Recently, we have been working on the development of Multipath TCP, a TCP extension that allows a TCP connection to use multiple IP addresses on multihomed hosts or mobile hosts. In practice, this TCP extension allows to group several TCP connections together so that the application on top of TCP has the illusion of sending and receiving data through a single MPTCP connection although the data is actually transported by different TCP connections. To provide this feature, and also cope with middleboxes such as NAT, Multipath TCP includes various mechanisms that significantly increase its complexity.
We have developed a prototype implementation of Multipath TCP in the Linux kernel ( http://inl.info.ucl.ac.be/mptcp ) and the standardisation work within the IETF is progressing well. There are currently two well identified use cases where Multipath TCP provides benefits over regular TCP :
- mobile devices such as smartphones
- datacenters where Multipath TCP can achieve a better performance than regular TCP
However, I am a bit concerned by the complexity of Multipath TCP and I'd like to be able to get some kind of validation that there are no corner cases in the current protocol specification. When I was a PhD student, I did some verification work with LOTOS bu I haven't used verification tools during the last fifteen years. One of my colleagues mentioned that Promela/Spin were probably the best approach to provide this kind of validation. I would be in particular interested in a validation of the connection establishment and release phases of MPTCP, a problem which is probably more tractable than a full validation of Multipath TCP.
Before starting to work on this, I'd like to know whether someone who has promela experience would be interested in working on such a topic or perhaps share an existing model of TCP in promela that could be reused ?
Best regards
Olivier Bonaventure
Pages: 1