Laura Bocchi
Senior Lecturer @ University of Kent
Laura is a Senior Lecturer in Computing at the University of Kent. She is interested in static and dynamic verification of communicating programs by using behavioural types (ie., types that describe communication behaviours). Her current research is on time-sensitive properties and reliability. She is currently a WP leader in the EU RISE project ‘BehAPI’ on behavioural APis, and in the EPSRC project 'Session Types for Reliable Distributed Systems (STARDUST)'.
Past Activities
Code BEAM V Europe
13.10 - 13.50
Compositional protocol engineering for communicating actors
In systems of communicating processes or actors, data types can be used to discipline the sorts of sent and received messages. Session types, in addition, can describe specific causalities and patterns among different send/receive actions (like application-level protocols). I will give an overview on recent and ongoing research about writing “good protocols” using session types and session types to yield correct implementations.
I will then focus on modular composition of protocols. Real-world communication protocols are often built out of simpler protocols that cater for some specific functionality (e.g., banking, authentication) or operate at different levels of abstraction (e.g., HTTP, POP). However much of the work used for program verification (e.g., session types) treat protocols as monolithic units.
I will show an approach to protocol composition, including a tool that extracts models from concurrent Erlang code into a protocol language based on session types, implements an algorithmic notion of protocol composition, and provides code generation from protocols. The purpose is greater modularisation and code reuse.
Code Mesh V
17.30 - 18.10
Protocol engineering for communicating actors
In systems of communicating processes or actors, data types can be used to discipline the sorts of sent and received messages. Behavioural types, in addition, can describe specific causalities and patterns among different send/receive actions (like application-level protocols). I will give an overview on recent and ongoing research about writing realisable behavioural types, especially those including time-constraints and deadlines, and use them to yield correct implementations (e.g., supporting implementation and verification) using programming languages like Erlang.
OBJECTIVES
Advocate the benefits of protocol awareness. Increase awareness of research and available verification techniques. Get all in the loop and discuss together about future directions.
AUDIENCE
Anyone interested in distributed communications.