Final Report of the COST-247 Action

ABRUPTLY-TERMINATED CONNECTIONS IN TCP -- A VERIFICATION EXAMPLE

Ina Schieferdecker

 GMD Fokus Hardenbergplatz 2 D-10623 Berlin Germany Tel: (030) 254 99 241 Fax: (030) 254 99 202 e-mail: ina@fokus.gmd.de

### Abstract:

The talk presented the verification of a functional misbehavior in TCP, that is one of the widely used transport protocols used in the Internet. The solution that was developed by I. Heavens is verified for its correctness. A model checking approach is used to verify TCP: the protocol is described in LOTOS and the requirements are given in the modal $\mu$-calculus. The verification uses the CADP tool set for automating the verification process.

This presentation has been given during the COST-247 International Workshop on Applied Formal Methods in System Design (Maribor, Slovenia, June 17--19, 1996).

COST-247 Working Group(s): 1-2