Time-sensitive protocol: Links From Design to Implementation
summary
Develops a formal link from timed protocol specs to implementable abstractions using Timed Session Types and Timed Automata, shows a typing system with virtual clocks that rejects time-unsafe implementations, and implements an executable calculus plus tests that observe blocking vs urgent receives. Introduces urgent receive semantics under which a session type composed with its dual enjoys progress (feasibility), models network latency with forwarder processes, and reports a working prototype and algorithms that catch subtle deadline violations.
AI-written summary · about
chapters (20)
- 0:00Intro
- 0:58The problem
- 4:03Well-structured interactions
- 6:05Asynchrony is complex
- 7:25"Good" Interaction Structures
- 10:20Communicating Automata
- 11:22The look of Session Types
- 13:14The use of Session Types
- 15:19Time brings trouble
- 17:27Duality & progress
- 19:04Duality & asynchronous communication
- 21:48Asynchronous receive
- 23:45Urgent receive semantics
- 25:22Objection
- 26:22A timed calculus
- 29:57Example
- 33:35Typing rules (in short)
- 34:48Type Checking with time
- 38:27Wrapping up (part 1)
- 40:16Wrapping up (part 2)
related talks
37mSession Types: A History and Applications
16mParameterized Verification of Disjunctive Timed Networks
35mNobody Knows What Time It Is
24mSynthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications
47mAdventures in Spacetime
15mTLC: Temporal Logic of Distributed Components
39mProtocol engineering for communicating actors
47mInteraction Protocols: It's all about good manners