OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

SysML Modeling and Formal Verification of the TCP Relentless Congestion Protocol

Saqui-Sannes, Pierre de and Diana, Rémi and Lochin, Emmanuel SysML Modeling and Formal Verification of the TCP Relentless Congestion Protocol. (2011) [Report] (Unpublished)

[img] (Document in English)

PDF ( Author's version) - Depositor and staff only - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
245kB

Abstract

The paper shares an experience in SysML modeling and formal verification of smart Internet protocols. The design trajectory includes requirement capture, use-case driven analysis, architectural design, and protocol machines description. The SysML model of the protocol is simulated and formally verified using TTool and UPPAAL. The paper uses an improved Relentless Congestion Mechanism as running example. The new RCC mechanisms revisits the lost retransmission detection scheme and better behaves in the high bandwidth delay networks that populate today’s Internet.

Item Type:Report
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE-SUPAERO (FRANCE)
Laboratory name:
Statistics:download
Deposited By: Emmanuel Lochin
Deposited On:12 Mar 2013 11:45

Repository Staff Only: item control page