Database of Case Studies Achieved Using CADP

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 our FTP 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


Last modified: Fri Feb 19 09:12:04 2016.


Back to the CADP case studies page