BRAVETTI , Mario

We survey our work on choreographies and behavioural contracts in multiparty interactions. In particular theories of behavioural contracts are presented which enable reasoning about correct service composition (contract compliance) and service substitutability (contract refinement preorder) under different assumptions concerning service...

Markovian process algebras allow for performance analysis by automatic generation of Continuous Time Markov Chains. The inclusion of exponential distribution rate information in process algebra terms, however, causes non trivial issues to arise in the definition of their semantics. As a consequence, technical settings previously considered do...

Milner's complete proof system for observational congruence is crucially based on the possibility to equate τ divergent expressions to non-divergent ones by means of the axiom recX.(τ.X + E) = recX.τ.E. In the presence of a notion of priority, where, e.g., actions of type δ have a lower priority than silent τ actions, this axiom is no longer...

We briefly recall results obtained in twenty years of research, spanning across the old and the new millennium, on the expressiveness of coordination languages and on behavioural contracts for Service-Oriented Computing. Then, we show how the techniques developed in those contexts are currently contributing to the clarification of aspects that...

We recall techniques, mainly based on the theory of process calculi, that we used to prove results in twenty years of research, spanning across the old and the new millennium, on the expressiveness of coordination languages and on behavioural contracts for Service-Oriented Computing. Then, we show how such techniques recently contributed to the...

We discuss the relationship between session types and be-havioural contracts under the assumption that processes communicate asynchronously. We show the existence of a fully abstract interpretation of session types into a fragment of contracts, that maps session subtyping into binary compliance-preserving contract refinement. In this way, the...

We study the relationship between session types and behavioural contracts, representing Communicating Finite State Machines (CFSMs), under the assumption that processes communicate asynchronously. Session types represent a syntax-based approach for the description of communication protocols, while behavioural contracts, formally expressing...

Session types are behavioural types for guaranteeing that concurrent programs are free from basic communication errors. Recent work has shown that asyn-chronous session subtyping is undecidable. However, since session types have become popular in mainstream programming languages in which asynchronous communication is the norm rather than the...

Session types are used to describe communication protocols in distributed systems and, as usual in type theories, session subtyping characterizes substitutability of the communicating processes. We investigate the (un)decidability of subtyping for session types in asynchronously communicating systems. We first devise a core undecidable...

Session types are widely used as abstractions of asynchronous message passing systems. Refinement for such abstractions is crucial as it allows improvements of a given component without compromising its compatibility with the rest of the system. In the context of session types, the most general notion of refinement is the asynchronous session...

In this paper we propose a new mechanism for Dynamic Rebinding, a particular kind of Dynamic Software Updating that focuses on modifying the workflow of a program. This mechanism is built upon the concurrency model of Concurrent Object Groups that is adopted in programming languages like Coboxes, Creol or ABS. Using this model, which extends...

We introduce a probabilistic extension of our previous work SPLA: a formal framework to specify and analyze software product lines. We use probabilistic information to identify those features that are more frequently used. This is done by computing the probability of having a feature in a specific software product line, from now on SPLA P. We...

Session types are becoming popular and have been integrated in several mainstream programming languages. Nevertheless, while many programming languages consider asynchronous fifo channel communication, the notion of subtyping used in session type implementations is the one defined by Gay and Hole for synchronous communication. This might be...

In this paper we introduce a framework for detecting anomalies in the clocks of the different components of a network of sensor stations connected with a central server for measuring of air quality. Local clocks of sensor stations can be advanced/delayed with respect to the central server clock and this situation provokes the inaccuracy in the...

We give two different notions of deadlock for systems based on active objects and futures. One is based on blocked objects and conforms with the classical definition of deadlock by Coffman, Jr. et al. The other one is an extended notion of deadlock based on blocked processes which is more general than the classical one. We introduce a technique...

Following previous work on the automated deployment of componentbased applications, we present a formal model specifically tailored for reasoning on the deployment of microservice architectures. The first result that we present is a formal proof of decidability of the problem of synthesizing optimal deployment plans for microservice...

International audience

Session types, types for structuring communication between endpoints in concurrent systems, are recently being integrated into mainstream programming languages. In practice, a very important notion for dealing with such types is that of subtyping, since it allows for typing larger classes of systems, where a program has not precisely the...

Microservices are highly modular and scalable Service Oriented Architectures. They underpin automated deployment practices like Continuous Deployment and Autoscaling. In this paper we formalize these practices and show that automated deployment-proven undecid-able in the general case-is algorithmically treatable for microservices. Our key...

Session types, types for structuring communication between endpoints in distributed systems, are recently being integrated into mainstream programming languages. In practice, a very important notion for dealing with such types is that of subtyping, since it allows for typing larger classes of system, where a program has not precisely the...

We develop a novel approach for run-time global adaptation of microservice applications, based on synthesis of architecture-level reconfiguration orchestrations. More precisely, we devise an algorithm for automatic reconfiguration that reaches a target system Maximum Computational Load by performing optimal deployment orchestrations. To...

In this work, we focus on by-design global scaling, a technique that, given a functional specification of a microservice architecture, or-chestrates the scaling of all its components, avoiding cascading slowdowns typical of uncoordinated, mainstream autoscaling. State-of-the-art by-design global scaling adopts a reactive approach to traffic...

We present a type-based analysis ensuring memory safety and object protocol completion in the Java-like language Mungo. Objects are annotated with usages, typestates-like specifications of the admissible sequences of method calls. The analysis entwines usage checking, controlling the order in which methods are called, with a static check...

No description

International audience