Timing is everything, so they say... Laura Bocchi discusses establishing relationships between protocols and their implementations, the focus of her talk, at Lambda World, is on developing systems where distributed components interact via asynchronous message passing. She especially focuses on time-sensitive protocols, where interactions are associated with time-constraints.
We look at two (partly-related) formal ways of describing protocols: Timed Session Types and Automata. Session Types are a powerful and effective technique for program verification; they allow to type-check programs against their communication behavior, other than on the type of messages. For Timed Automata, the relationship between protocols and (abstractions of) programs can be expressed as a refinement relation between more and less abstract models, giving concrete guidelines on how to implement timed protocols while preserving the intended behavior and progress. I will discuss recent theories, learnings, open challenges, and future directions.