Prior to the summer school in Leicester, a one-day workshop shall be organised on 6th July, where various speakers from all around the globe shall be giving short talks on relevant subjects.
Location
The workshop will be held in room KEN LT2, Ken Edwards Building, University of Leicester
Programme
10.30 — Adventures in Monitorability: From Branching to Linear Time and Back Again
Speaker: Adrian Francalanza (UOM)
Abstract: We establish a comprehensive theory of runtime monitorability for Hennessy-Milner logic with recursion, a very expressive variant of the modal μ-calculus. We investigate the monitorability of that logic with a linear-time semantics and then compare the obtained results with ones that were previously presented in the literature for a branching-time setting. Our work establishes an expressiveness hierarchy of monitorable fragments of Hennessy-Milner logic with recursion in a linear-time setting and exactly identifies what kinds of guarantees can be given using runtime monitors for each fragment in the hierarchy. Each fragment is shown to be complete, in the sense that it can express all properties that can be monitored under the corresponding guarantees. The study is carried out using a principled approach to monitoring that connects the semantics of the logic and the operational semantics of monitors. The proposed framework supports the automatic, compositional synthesis of correct monitors from monitorable properties.
11.00 — Behavioural Types Make Object-Oriented Programs Go Right
Speaker: Antonio Ravara (NOVA)
Abstract: I’ll present a notion of types to Java-like languages that allow to declare the intended usage protocol of objects of a class. The type system ensures not only the absence of the usual “method-not-understood” error, but also other safety properties like memory safety and a liveness property – protocol completion. Class usage protocols might be written as terms of a context-free grammar or defined as automata. Bi-directional transformations allow the programmer to start with which she prefers and refine the specification with the help of the transformations, as they provide visualisation. From the usage protocols it is possible to get skeletons of Java
code. We are also working on getting the usage protocols from the
usual Java code.
11.30 — Resource sharing via capability-based multiparty session types
Speaker: Adriana Laura Voinea (UGLA)
Abstract: Multiparty Session Types (MPST) are a type formalism used to model communication protocols among components in distributed systems, by specifying type and direction of data transmitted. It is standard for multiparty session type systems to use access control based on linear or affine types. While useful in offering strong guarantees of communication safety and session fidelity, linearity (resp. affinity) run into the well-known problem of inflexible programming, excluding scenarios that make use of shared channels or need to store channels into shared data structures. In this paper, we develop capability-based access control for multiparty session types. This gives rise to a more flexible session type system, which allows channel references to be shared and stored in persistent data structures. We prove type safety and illustrate the expressiveness of our type system through examples.
12.00 — Towards a Logic of Forwarders
Speaker: Marco Carbone (ITU)
Abstract: I will talk about ongoing work on a fragment of linear logic that is in a Curry-Howard correspondence with processes that forward messages and, as a consequence, with multiparty sessions types.
12.30 – 14.30 Lunch
14.30 — A behavioural model of fishes & ponds
Speaker: Roland Kuhn & Hernan Melgratti (UBA)
Abstract: We report on a model of the communication infrastructure
currently developed at Actyx.
15.00 — Causal-Consistent Reversible Debugging for Message Passing Programs
Speaker: Ivan Lanese (UNIBO)
Abstract: Causal-consistent reversible debugging is an innovative technique for debugging concurrent systems. It allows one to go back in the execution focusing on the actions that most likely caused a visible misbehavior. When such an action is selected, the debugger undoes it, including all and only its consequences. This operation is called a causal-consistent rollback. In this way, the user can avoid being distracted by the actions of other, unrelated processes. The dual notion of causal-consistent rollback is causal-consistent replay. It allows the user to record an execution of a running program and, in contrast to traditional replay debuggers, to reproduce a visible misbehavior inside the debugger including all and only its causes. We present a unified framework for debugging message passing Erlang systems that combines both causal-consistent replay and causal consistent rollback.
15.30 — Automatic Quality-of-Service evaluation in Service-Oriented Computing
Speaker: Agustín Martinez Suñé
Abstract: Formally describing and analysing quantitative requirements of software components might be important in software engineering; in the paradigm of API-based software systems might be vital. Quantitative requeriments can be thought as characterising the Quality of Service – QoS provided by a service thus, useful as a way of classifying and ranking them according to specific needs. An efficient and automatic analysis of this type of requirements could provide the means for enabling dynamic establishing of Service Level Agreements – SLA, allowing for the automatisation of the Service Broker. In this we will show the use of a language for describing QoS contracts based on convex specification and discuss:
- a two-phase analysis procedure for evaluating contract satisfaction based on the state of the art techniques used for hybrid system verification, where the first phase of the procedure responds to the observation that when services are registered in repositories and their contracts are stored for subsequent use in negotiating SLAs, thus contract minimisation might lead to great efficiency gain when the second, and recurrent, phase of determining QoS compliance is run, and
- a technique for QoS ranking for services whose provision contract only partially satisfy a given requirement contract.