BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Emilio Tuosto

Emilio Tuosto appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
Logic in Computer ScienceProgramming LanguagesDistributed, Parallel, and Cluster ComputingSoftware EngineeringFormal Languages and Automata TheoryNetworking and Internet Architecture

Catalog footprint

What is connected

17works
6topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

17 published item(s)

preprint2022arXiv

Design-by-Contract for Flexible Multiparty Session Protocols -- Extended Version

Choreographic models support a correctness-by-construction principle in distributed programming. Also, they enable the automatic generation of correct message-based communication patterns from a global specification of the desired system behaviour. In this paper we extend the theory of choreography automata, a choreographic model based on finite-state automata, with two key features. First, we allow participants to act only in some of the scenarios described by the choreography automaton. While this seems natural, many choreographic approaches in the literature, and choreography automata in particular, forbid this behaviour. Second, we equip communications with assertions constraining the values that can be communicated, enabling a design-by-contract approach. We provide a toolchain allowing to exploit the theory above to generate APIs for TypeScript web programming. Programs communicating via the generated APIs follow, by construction, the prescribed communication pattern and are free from communication errors such as deadlocks.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

On Composing Communicating Systems

Communication is an essential element of modern software, yet programming and analysing communicating systems are difficult tasks. A reason for this difficulty is the lack of compositional mechanisms that preserve relevant communication properties. This problem has been recently addressed for the well-known model of communicating systems, that is sets of components consisting of finite-state machines capable of exchanging messages. The main idea of this approach is to take two systems, select a participant from each of them, and derive from those participants a pair of coupled gateways connecting the two systems. More precisely, a message directed to one of the gateways is forwarded to the gateway in the other system, which sends it to the other system. It has been shown that, under some suitable compatibility conditions between gateways, this composition mechanism preserves deadlock freedom for asynchronous as well as symmetric synchronous communications (where sender and receiver play the same part in determining which message to exchange). This paper considers the case of asymmetric synchronous communications where senders decide independently which message should be exchanged. We show here that preservation of lock freedom requires sequentiality of gateways, while this is not needed for preservation of either deadlock freedom or strong lock freedom.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

An Abstract Framework for Choreographic Testing

We initiate the development of a model-driven testing framework for message-passing systems. The notion of test for communicating systems cannot simply be borrowed from existing proposals. Therefore, we formalize a notion of suitable distributed tests for a given choreography and devise an algorithm that generates tests as projections of global views. Our algorithm abstracts away from the actual projection operation, for which we only set basic requirements. The algorithm can be instantiated by reusing existing projection operations (designed to generate local implementations of global models) as they satisfy our requirements. Finally, we show the correctness of the approach and validate our methodology via an illustrative example.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Probabilistic Analysis of Binary Sessions

We study a probabilistic variant of binary session types that relate to a class of Finite-State Markov Chains. The probability annotations in session types enable the reasoning on the probability that a session terminates successfully, for some user-definable notion of successful termination. We develop a type system for a simple session calculus featuring probabilistic choices and show that the success probability of well-typed processes agrees with that of the sessions they use. To this aim, the type system needs to track the propagation of probabilistic choices across different sessions.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Towards Refinable Choreographies

We investigate refinement in the context of choreographies. We introduce refinable global choreographies allowing for the underspecification of protocols, whose interactions can be refined into actual protocols. Arbitrary refinements may spoil well-formedness, that is the sufficient conditions that guarantee a protocol to be implementable. We introduce a typing discipline that enforces well-formedness of typed choreographies. Then we unveil the relation among refinable choregraphies and their admissible refinements in terms of an axiom scheme.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

An Abstract Semantics of the Global View of Choreographies

We introduce an abstract semantics of the global view of choreographies. Our semantics is given in terms of pre-orders and can accommodate different lower level semantics. We discuss the adequacy of our model by considering its relation with communicating machines, that we use to formalise the local view. Interestingly, our framework seems to be more expressive than others where semantics of global views have been considered. This will be illustrated by discussing some interesting examples.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Communicating machines as a dynamic binding mechanism of services

Distributed software is becoming more and more dynamic to support applications able to respond and adapt to the changes of their execution environment. For instance, service-oriented computing (SOC) envisages applications as services running over globally available computational resources where discovery and binding between them is transparently performed by a middleware. Asynchronous Relational Networks (ARNs) is a well-known formal orchestration model, based on hypergraphs, for the description of service-oriented software artefacts. Choreography and orchestration are the two main design principles for the development of distributed software. In this work, we propose Communicating Relational Networks (CRNs), which is a variant of ARNs, but relies on choreographies for the characterisation of the communicational aspects of a software artefact, and for making their automated analysis more efficient.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

From Orchestration to Choreography through Contract Automata

We study the relations between a contract automata and an interaction model. In the former model, distributed services are abstracted away as automata - oblivious of their partners - that coordinate with each other through an orchestrator. The interaction model relies on channel-based asynchronous communication and choreography to coordinate distributed services. We define a notion of strong agreement on the contract model, exhibit a natural mapping from the contract model to the interaction model, and give conditions to ensure that strong agreement corresponds to well-formed choreography.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Nominal Regular Expressions for Languages over Infinite Alphabets. Extended Abstract

We propose regular expressions to abstractly model and study properties of resource-aware computations. Inspired by nominal techniques -- as those popular in process calculi -- we extend classical regular expressions with names (to model computational resources) and suitable operators (for allocation, deallocation, scoping of, and freshness conditions on resources). We discuss classes of such nominal regular expressions, show how such expressions have natural interpretations in terms of languages over infinite alphabets, and give Kleene theorems to characterise their formal languages in terms of nominal automata.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

On Recovering from Run-time Misbehaviour in ADR

We propose a monitoring mechanism for recording the evolution of systems after certain computations, maintaining the history in a tree-like structure. Technically, we develop the monitoring mechanism in a variant of ADR (after Architectural Design Rewriting), a rule-based formal framework for modelling the evolution of architectures of systems. The hierarchical nature of ADR allows us to take full advantage of the tree-like structure of the monitoring mechanism. We exploit this mechanism to formally define new rewriting mechanisms for ADR reconfiguration rules. Also, by monitoring the evolution we propose a way of identifying which part of a system has been affected when unexpected run-time behaviours emerge. Moreover, we propose a methodology to suggest reconfigurations that could potentially lead the system in a non-erroneous state.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Enforcing Architectural Styles in Presence of Unexpected Distributed Reconfigurations

Architectural Design Rewriting (ADR, for short) is a rule-based formal framework for modelling the evolution of architectures of distributed systems. Rules allow ADR graphs to be refined. After equipping ADR with a simple logic, we equip rules with pre- and post-conditions; the former constraints the applicability of the rules while the later specifies properties of the resulting graphs. We give an algorithm to compute the weakest pre-condition out of a rule and its post-condition. On top of this algorithm, we design a simple methodology that allows us to select which rules can be applied at the architectural level to reconfigure a system so to regain its architectural style when it becomes compromised by unexpected run-time reconfigurations.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

On the realizability of contracts in dishonest systems

We develop a theory of contracting systems, where behavioural contracts may be violated by dishonest participants after they have been agreed upon - unlike in traditional approaches based on behavioural types. We consider the contracts of \cite{CastagnaPadovaniGesbert09toplas}, and we embed them in a calculus that allows distributed participants to advertise contracts, reach agreements, query the fulfilment of contracts, and realise them (or choose not to). Our contract theory makes explicit who is culpable at each step of a computation. A participant is honest in a given context S when she is not culpable in each possible interaction with S. Our main result is a sufficient criterion for classifying a participant as honest in all possible contexts.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Synthesising Choreographies from Local Session Types (extended version)

Designing and analysing multiparty distributed interactions can be achieved either by means of a global view (e.g. in choreography-based approaches) or by composing available computational entities (e.g. in service orchestration). This paper proposes a typing systems which allows, under some conditions, to synthesise a choreography (i.e. a multiparty global type) from a set of local session types which describe end-point behaviours (i.e. local types).

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

A Modular Toolkit for Distributed Interactions

We discuss the design, architecture, and implementation of a toolkit which supports some theories for distributed interactions. The main design principles of our architecture are flexibility and modularity. Our main goal is to provide an easily extensible workbench to encompass current algorithms and incorporate future developments of the theories. With the help of some examples, we illustrate the main features of our toolkit.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Amending Contracts for Choreographies

Distributed interactions can be suitably designed in terms of choreographies. Such abstractions can be thought of as global descriptions of the coordination of several distributed parties. Global assertions define contracts for choreographies by annotating multiparty session types with logical formulae to validate the content of the exchanged messages. The introduction of such constraints is a critical design issue as it may be hard to specify contracts that allow each party to be able to progress without violating the contract. In this paper, we propose three methods that automatically correct inconsistent global assertions. The methods are compared by discussing their applicability and the relationships between the amended global assertions and the original (inconsistent) ones.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Contracts in distributed systems

We present a parametric calculus for contract-based computing in distributed systems. By abstracting from the actual contract language, our calculus generalises both the contracts-as-processes and contracts-as-formulae paradigms. The calculus features primitives for advertising contracts, for reaching agreements, and for querying the fulfilment of contracts. Coordination among principals happens via multi-party sessions, which are created once agreements are reached. We present two instances of our calculus, by modelling contracts as (i) processes in a variant of CCS, and (ii) as formulae in a logic. With the help of a few examples, we discuss the primitives of our calculus, as well as some possible variants.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

Toward a Formal Semantics for Autonomic Components

Autonomic management can improve the QoS provided by parallel/ distributed applications. Within the CoreGRID Component Model, the autonomic management is tailored to the automatic - monitoring-driven - alteration of the component assembly and, therefore, is defined as the effect of (distributed) management code. This work yields a semantics based on hypergraph rewriting suitable to model the dynamic evolution and non-functional aspects of Service Oriented Architectures and component-based autonomic applications. In this regard, our main goal is to provide a formal description of adaptation operations that are typically only informally specified. We contend that our approach makes easier to raise the level of abstraction of management code in autonomic and adaptive applications.

0 citations0 reviewsNo code linkedOpen access