|Final Report of the COST-247 Action|
ABRUPTLY-TERMINATED CONNECTIONS IN TCP -- A VERIFICATION EXAMPLE
|Tel: (030) 254 99 241|
|Fax: (030) 254 99 202|
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.