|
| 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 |
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
This Page was prepared by Mark Jorgensen.
Back to the VASY Home page