BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Proven performance guarantees in Time Sensitive Networking and Det
 erministic Networking
DTSTART:20190206T110000
DTEND:20190206T130000
DTSTAMP:20260407T064047Z
UID:d6738fcdf175c2fe34ec76328f5e158273eab9b6b3c1e539923ea49b
CATEGORIES:Conferences - Seminars
DESCRIPTION:Ehsan Mohammadpour\nEDIC candidacy exam\nExam president: Prof.
  Patrick Thiran\nThesis advisor: Prof. Jean-Yves Le Boudec\nCo-examiner: P
 rof. Viktor Kuncak\n\nAbstract\n Time-Sensitive Networking (TSN) and Dete
 rministic Networking (DetNet) define mechanisms for zero packet loss and b
 ounded end-to-end latency. A known technique to compute these bounds is ne
 twork calculus. Classical network calculus provides pessimistic bounds in 
 feed-forward networks with per-class queuing due to the effect of multiple
 xing: burstiness of competing flows are accounted multiple times in the bo
 und calculations. To address this issue\, Pay-Multiplexing-Only-Once (PMOO
 ) property was introduced to improve the latency bound by accounting the b
 urstiness of competing flows once in the feed-forward networks. However\, 
 it does not apply to non-feed-forward networks with circular dependency du
 e to burstiness cascade: individual flows may see their burstiness increas
 e due to sharing one queue\, that in turn causes burstiness of the downstr
 eam flows. In order to avoid this problem\, the interleaved regulator was 
 introduced to perform reshaping for the flows leading to have fresh flows 
 at every hop. Interleaved regulators aggregate flows in one queue\, while 
 reshaping the packet at the head of the queue based on its flows regulatio
 n policy. Accordingly\, latency and backlog bounds in any FIFO-based netwo
 rks are obtained. Due to criticality of TSN/DetNet applications\, it is ne
 cessary to certify the obtained bounds. Isabelle/HOL is a semi-automatic s
 oftware framework to certify the theorems based on a trusted kernel\, user
 -defined syntax and proof rules. This report also describes a research pla
 n based on the three selected papers. To this end\, rigorous theorems to c
 ompute latency and backlog bounds by using interleaved regulators in TSN/D
 etNet\, a routing algorithm for TSN/DetNet flows\, certification of the th
 eorem with the Isabelle/HOL\, and a TSN/DetNet simulator will be reported.
 \n\nBackground papers\nA Theory of Traffic Regulators for Deterministic Ne
 tworks with Application to Interleaved Regulators\, by Prof J-Y.\, Le Boud
 ec\nImproving Performance Bounds in Feed-Forward Networks by Paying Multip
 lexing Only Once\, by J.B.\, Schmitt et al.\nCertifying Network Calculus i
 n a Proof Assistant\, by E. Mabille et al.\n\n\n 
LOCATION:INF 018 https://plan.epfl.ch/?room=INF018
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR
