Verify me if you can: Timers, Actors and Session Types

We propose a dynamic verification framework for protocols in distributed systems. The framework is based on Scribble, a tool-chain for design and verification of choreographies based on multiparty session types. Scribble protocols enjoy safety and liveness properties such as deadlock-freedom and progress between distributed endpoints. We have implemented dedicated runtime monitors that check each interaction complies with the corresponding Scribble specification. In this talk, we present the verification framework and emphasise on two recent developments that leverage its applicability. First, we explain the challenges of extending session types for real-time interactions. We show two properties - feasibility and wait-freedom that guarantee progress for time-dependent applications. In the second part of the talk, we show how to apply session types verification to a popular concurrency model - actors programming. We incorporate sessions to actors by introducing minimum additions to the model such as the notion of actor roles and protocol mailboxes. The usage of multiple roles allows safe cooperative interconcurrency in a single actor.