Lambda World 2019 - Time-sensitive protocol: Links From Design to Implementation - Laura Bocchi
This talk will centre on developing systems where distributed components interact via asynchronous message passing, and need to follow specific interaction patterns, e.g., ad-hoc application-level protocols, such as POP2.
I will discuss ongoing work towards establishing relationships between protocols and their implementations, focussing on time-sensitive protocols, where interactions are associated to time-constraints. We will 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 behaviour, other than on the type of the 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 behaviour and progress.
I will discuss recent theories, learnings, open challenges, and future directions.