Abruptly Terminated Connections in TCP

Organisation:	GMD-Fokus, Berlin, Germany
Method:	LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Network protocols, Internet.
Period:	1996
Size:	300 Lines of LOTOS
Description:	Only recently a functional error in the TCP mechanism for closing connections was recognized. The question we asked ourselves was whether it would have been possible to detect this misbehaviour by applying formal verification without any use of the knowledge about the error. We attacked the problem in the framework of functional behaviour specification of the protocol, temporal logic specification of the correctness requirements, and verification by the use of model checking algorithms. The functional behaviour of TCP was specified in LOTOS. A model for the specification was produced compositionally, by generating individually the models of the TCP entities and the medium using CAESAR, before combining them using ALDEBARAN. The correctness requirements were specified in the modal mu-calculus, and then evaluated on the model using EVALUATOR.
Conclusions:	During the specification phase, some bugs and ambiguities were detected in the original TCP specification and resolved according to a reference implementation. The complete TCP specification could not be analyzed due state space explosion: some assumptions were made to reduce the size of the model. Nonetheless, it showed that tools for automatic verification are powerful enough to analyze problems of practical needs. TCP is a good candidate to explore methods for timed verification, since the protocol makes intensive use of timers.
Publications:	Ina Schieferdecker. Abruptly Terminated Connections in TCP - A Verification Example. In Z. Brezocnik and T. Kapus, editors, Proceedings of the COST 247 International Workshop on Applied Formal Methods in System Design (Maribor, Slovenia), pages 136-145. University of Maribor, Slovenia, June 1996. Available on-line at: http://www.el.feri.uni-mb.si/lms/cost247/proc/schieferdecker.ps and from the CADP Web site in PDF or PostScript
Contact:	Ina Schieferdecker GMD Fokus Hardenbergplatz 2 D-10623 Berlin Germany Tel: +(30) 254 99 241 Fax: +(30) 254 99 202 e-mail: ina@fokus.gmd.de
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page