Design by Contract for multiparty distributed interactions: static and dynamic validation
- Speaker: Dr Laura Bocchi, Department of Computing, Imperial College London.
- Date: Wednesday, 6 November 2013 from 16:30 to 17:30
- Location: Room 160, Birkbeck Main Building
Multiparty session types (MPSTs) are a typing theory for protocols involving two or more participants communicating via asynchronous message passing (aka choreographies). MPSTs enable tractable and modular verification of properties on the types of exchanged data and on the causality of the interactions. This talk will centre on the extension of MPSTs with logical formulae, called multiparty session assertions (MPSAs), which yields an assertion method for session communication based on Design by Contract (DbC). DbC promotes reliable software development through the elaboration of type signatures with logical formulae. Trough the elaboration of MPSTs with predicates, we allow the verification of a richer set of properties (wrt MPSTs), namely on the contents of the exchanged messages, on the selected branches, and recursion invariants. I will talk about static verification of distributed applications against MPSAs, which works under the assumption that all endpoints are well-typed, and about a recent extensions of our framework to support run-time safety enforcement in presence of untrusted endpoints. This extension is motivated by its practical application to a large-scale infrastructure for ocean observation.