-
SEArch: an execution infrastructure for service-based software systems
Authors:
Carlos G. Lopez Pombo,
Pablo Montepagano,
Emilio Tuosto
Abstract:
The shift from monolithic applications to composition of distributed software initiated in the early twentieth, is based on the vision of software-as-service. This vision, found in many technologies such as RESTful APIs, advocates globally available services cooperating through an infrastructure providing (access to) distributed computational resources. Choreographies can support this vision by ab…
▽ More
The shift from monolithic applications to composition of distributed software initiated in the early twentieth, is based on the vision of software-as-service. This vision, found in many technologies such as RESTful APIs, advocates globally available services cooperating through an infrastructure providing (access to) distributed computational resources. Choreographies can support this vision by abstracting away local computation and rendering interoperability with message-passing: cooperation is achieved by sending and receiving messages. Following this choreographic paradigm, we develop SEArch, after Service Execution Architecture, a language-independent execution infrastructure capable of performing transparent dynamic reconfiguration of software artefacts. Choreographic mechanisms are used in SEArch to specify interoperability contracts, thus providing the support needed for automatic discovery and binding of services at runtime.
△ Less
Submitted 30 April, 2024;
originally announced April 2024.
-
COTS: Connected OpenAPI Test Synthesis for RESTful Applications
Authors:
Christian Bartolo Burlò,
Adrian Francalanza,
Alceste Scalas,
Emilio Tuosto
Abstract:
We present a novel model-driven approach for testing RESTful applications. We introduce a (i) domain-specific language for OpenAPI specifications and (ii) a tool to support our methodology. Our DSL is inspired by session types and enables the modelling of communication protocols between a REST client and server. Our tool, dubbed COTS, generates (randomised) model-based test executions and reports…
▽ More
We present a novel model-driven approach for testing RESTful applications. We introduce a (i) domain-specific language for OpenAPI specifications and (ii) a tool to support our methodology. Our DSL is inspired by session types and enables the modelling of communication protocols between a REST client and server. Our tool, dubbed COTS, generates (randomised) model-based test executions and reports software defects. We evaluate the effectiveness of our approach by applying it to test several open source applications. Our findings indicate that our methodology can identify nuanced defects in REST APIs and achieve comparable or superior code coverage when compared to much larger handcrafted test suites.
△ Less
Submitted 30 April, 2024;
originally announced April 2024.
-
TRAC: a tool for data-aware coordination (with an application to smart contracts)
Authors:
Joao Afonso,
Elvis Konjoh Selabi,
Maurizio Murgia,
Antonio Ravara,
Emilio Tuosto
Abstract:
We propose TRAC, a tool for the specification and verification of coordinated multiparty distributed systems. Relying on finite-state machines (FSMs) where transition labels look like Hoare triples, \thetool can specify the coordination of the participants of a distributed protocol for instance an execution model akin blockchain smart contracts (SCs). In fact, the transitions of our FSMs yield gua…
▽ More
We propose TRAC, a tool for the specification and verification of coordinated multiparty distributed systems. Relying on finite-state machines (FSMs) where transition labels look like Hoare triples, \thetool can specify the coordination of the participants of a distributed protocol for instance an execution model akin blockchain smart contracts (SCs). In fact, the transitions of our FSMs yield guards, and assignments over data variables, and with participants binders. The latter allow us to model scenarios with an unbounded number of participants which can vary at run-time. We introduce a notion of well-formedness to rule out meaningless or problematic specifications. This notion is verified with TRAC and demonstrated on several case studies borrowed from the smart contracts domain. Then, we evaluate the performance of TRAC using a set of randomised examples, studying the correlations between the features supported and the time taken to decide well-formedness.
△ Less
Submitted 30 April, 2024;
originally announced April 2024.
-
MoCheQoS: Automated Analysis of Quality of Service Properties of Communicating Systems
Authors:
Carlos G. Lopez Pombo,
Agustín E. Martinez Suñé,
Emilio Tuosto
Abstract:
We present MoCheQoS, a bounded model checker to analyse (QoS) properties of message-passing systems. Building on the dynamic temporal logic, the choreographic model, and the bounded model checking algorithm defined in our ICTAC 2023 paper, MoCheQoS enables the static analysis of QoS properties of systems built out from the composition of services. We consider QoS properties on measurable applicati…
▽ More
We present MoCheQoS, a bounded model checker to analyse (QoS) properties of message-passing systems. Building on the dynamic temporal logic, the choreographic model, and the bounded model checking algorithm defined in our ICTAC 2023 paper, MoCheQoS enables the static analysis of QoS properties of systems built out from the composition of services. We consider QoS properties on measurable application-level attributes as well as resource consumption metrics for example those relating monetary cost to memory usage. The implementation of the tool is accompanied by an experimental evaluation. More precisely, we present two case studies meant to evaluate the applicability of MoCheQoS; the first is based on the AWS cloud while the second analyses a communicating system automatically extracted from code. Additionally, we consider synthetically generated experiments to assess the scalability of MoCheQoS. These experiments showed that our model can faithfully capture and effectively analyse QoS properties in industrial-strength scenarios.
△ Less
Submitted 28 June, 2024; v1 submitted 2 November, 2023;
originally announced November 2023.
-
A Dynamic Temporal Logic for Quality of Service in Choreographic Models
Authors:
Carlos G. Lopez Pombo,
Agustín E. Martinez Suñé,
Emilio Tuosto
Abstract:
We propose a framework for expressing and analyzing the Quality of Service (QoS) of message-passing systems using a choreographic model that consists of g-choreographies and Communicating Finite State machines (CFSMs). The following are our three main contributions: (I) an extension of CFSMs with non-functional contracts to specify quantitative constraints of local computations, (II) a dynamic tem…
▽ More
We propose a framework for expressing and analyzing the Quality of Service (QoS) of message-passing systems using a choreographic model that consists of g-choreographies and Communicating Finite State machines (CFSMs). The following are our three main contributions: (I) an extension of CFSMs with non-functional contracts to specify quantitative constraints of local computations, (II) a dynamic temporal logic capable of expressing QoS, properties of systems relative to the g-choreography that specifies the communication protocol, (III) the semi-decidability of our logic which enables a bounded model-checking approach to verify QoS property of communicating systems.
△ Less
Submitted 6 November, 2023; v1 submitted 2 November, 2023;
originally announced November 2023.
-
Behavioural Types for Local-First Software
Authors:
Roland Kuhn,
Hernán Melgratti,
Emilio Tuosto
Abstract:
Peer-to-peer systems are the most resilient form of distributed computing, but the design of robust protocols for their coordination is difficult. This makes it hard to specify and reason about global behaviour of such systems. This paper presents swarm protocols to specify such systems from a global viewpoint. Swarm protocols are projected to machines, that is local specifications of peers.
We…
▽ More
Peer-to-peer systems are the most resilient form of distributed computing, but the design of robust protocols for their coordination is difficult. This makes it hard to specify and reason about global behaviour of such systems. This paper presents swarm protocols to specify such systems from a global viewpoint. Swarm protocols are projected to machines, that is local specifications of peers.
We take inspiration from behavioural types with a key difference: peers communicate through an event notification mechanism rather than through point-to-point message passing. Our goal is to adhere to the principles of local-first software where network devices collaborate on a common task while retaining full autonomy: every participating device can locally make progress at all times, not encumbered by unavailability of other devices or network connections. This coordination-free approach leads to inconsistencies that may emerge during computations. Our main result shows that under suitable well-formedness conditions for swarm protocols consistency is eventually recovered and the locally observable behaviour of conforming machines will eventually match the global specification.
The model we propose elaborates on an existing industrial platform and provides the basis for tool support (sketched here and fully described in a companion artifact paper), wherefore we consider this work to be a viable step towards reasoning about local-first and peer-to-peer software systems.
△ Less
Submitted 8 May, 2023;
originally announced May 2023.
-
PSTMonitor: Monitor Synthesis from Probabilistic Session Types
Authors:
Christian Bartolo Burlò,
Adrian Francalanza,
Alceste Scalas,
Catia Trubiani,
Emilio Tuosto
Abstract:
We present PSTMonitor, a tool for the run-time verification of quantitative specifications of message-passing applications, based on probabilistic session types. The key element of PSTMonitor is the detection of executions that deviate from expected probabilistic behaviour. Besides presenting PSTMonitor and its operation, the paper analyses its feasibility in terms of the runtime overheads it indu…
▽ More
We present PSTMonitor, a tool for the run-time verification of quantitative specifications of message-passing applications, based on probabilistic session types. The key element of PSTMonitor is the detection of executions that deviate from expected probabilistic behaviour. Besides presenting PSTMonitor and its operation, the paper analyses its feasibility in terms of the runtime overheads it induces.
△ Less
Submitted 15 December, 2022; v1 submitted 14 December, 2022;
originally announced December 2022.
-
A Theory of Formal Choreographic Languages
Authors:
Franco Barbanera,
Ivan Lanese,
Emilio Tuosto
Abstract:
We introduce a meta-model based on formal languages, dubbed formal choreographic languages, to study message-passing systems. Our framework allows us to generalise standard constructions from the literature and to compare them. In particular, we consider notions such as global view, local view, and projections from the former to the latter. The correctness of local views projected from global view…
▽ More
We introduce a meta-model based on formal languages, dubbed formal choreographic languages, to study message-passing systems. Our framework allows us to generalise standard constructions from the literature and to compare them. In particular, we consider notions such as global view, local view, and projections from the former to the latter. The correctness of local views projected from global views is characterised in terms of a closure property. We consider a number of communication properties -- such as (dead)lock-freedom -- and give conditions on formal choreographic languages to guarantee them. Finally, we show how formal choreographic languages can capture existing formalisms; specifically we consider communicating finite-state machines, choreography automata, and multiparty session types. Notably, formal choreographic languages, differently from most approaches in the literature, can naturally model systems exhibiting non-regular behaviour.
△ Less
Submitted 1 August, 2023; v1 submitted 15 October, 2022;
originally announced October 2022.
-
On Composing Communicating Systems
Authors:
Franco Barbanera,
Ivan Lanese,
Emilio Tuosto
Abstract:
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 mac…
▽ More
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.
△ Less
Submitted 9 August, 2022;
originally announced August 2022.
-
Design-by-Contract for Flexible Multiparty Session Protocols -- Extended Version
Authors:
Lorenzo Gheri,
Ivan Lanese,
Neil Sayers,
Emilio Tuosto,
Nobuko Yoshida
Abstract:
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 all…
▽ More
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.
△ Less
Submitted 13 May, 2022;
originally announced May 2022.
-
Towards Probabilistic Session-Type Monitoring
Authors:
Christian Bartolo Burlò,
Adrian Francalanza,
Alceste Scalas,
Catia Trubiani,
Emilio Tuosto
Abstract:
We present a tool-based approach for the runtime analysis of communicating processes grounded on probabilistic binary session types. We synthesise a monitor out of a probabilistic session type where each choice point is decorated by a probability distribution. The monitor observes the execution of a process, infers its probabilistic behaviour and issues warnings when the observed behaviour deviate…
▽ More
We present a tool-based approach for the runtime analysis of communicating processes grounded on probabilistic binary session types. We synthesise a monitor out of a probabilistic session type where each choice point is decorated by a probability distribution. The monitor observes the execution of a process, infers its probabilistic behaviour and issues warnings when the observed behaviour deviates from the one specified by the probabilistic session type.
△ Less
Submitted 19 July, 2021;
originally announced July 2021.
-
Composition of choreography automata
Authors:
Franco Barbanera,
Ivan Lanese,
Emilio Tuosto
Abstract:
Choreography automata are an automata-based model of choreographies, that we show to be a compositional one. Choreography automata represent global views of choreographies (and rely on the well-known model of communicating finite-state machines to model local behaviours). The projections of well-formed global views are live as well as lock- and deadlock-free. In the class of choreography automata…
▽ More
Choreography automata are an automata-based model of choreographies, that we show to be a compositional one. Choreography automata represent global views of choreographies (and rely on the well-known model of communicating finite-state machines to model local behaviours). The projections of well-formed global views are live as well as lock- and deadlock-free. In the class of choreography automata we define an internal operation of {\em composition}, which connects two global views via roles acting as interfaces. We show that under mild conditions the composition of well-formed choreography automata is well-formed. The composition operation enables for a flexible modular mechanism at the design level.
△ Less
Submitted 14 July, 2021;
originally announced July 2021.
-
Towards Refinable Choreographies
Authors:
Ugo de'Liguoro,
Hernán Melgratti,
Emilio Tuosto
Abstract:
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 ty** discipline that enforces well-formed…
▽ More
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 ty** 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.
△ Less
Submitted 16 September, 2020;
originally announced September 2020.
-
An Abstract Framework for Choreographic Testing
Authors:
Alex Coto,
Roberto Guanciale,
Emilio Tuosto
Abstract:
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 p…
▽ More
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.
△ Less
Submitted 16 September, 2020;
originally announced September 2020.
-
Probabilistic Analysis of Binary Sessions
Authors:
Omar Inverso,
Hernán Melgratti,
Luca Padovani,
Catia Trubiani,
Emilio Tuosto
Abstract:
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 s…
▽ More
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.
△ Less
Submitted 23 July, 2020;
originally announced July 2020.
-
On Learning Nominal Automata with Binders
Authors:
Yi Xiao,
Emilio Tuosto
Abstract:
We investigate a learning algorithm in the context of nominal automata, an extension of classical automata to alphabets featuring names. This class of automata captures nominal regular languages; analogously to the classical language theory, nominal automata have been shown to characterise nominal regular expressions with binders. These formalisms are amenable to abstract modelling resource-aware…
▽ More
We investigate a learning algorithm in the context of nominal automata, an extension of classical automata to alphabets featuring names. This class of automata captures nominal regular languages; analogously to the classical language theory, nominal automata have been shown to characterise nominal regular expressions with binders. These formalisms are amenable to abstract modelling resource-aware computations. We propose a learning algorithm on nominal regular languages with binders. Our algorithm generalises Angluin's L* algorithm with respect to nominal regular languages with binders. We show the correctness and study the theoretical complexity of our algorithm.
△ Less
Submitted 12 September, 2019;
originally announced September 2019.
-
Interface Automata for Choreographies
Authors:
Hao Zeng,
Alexander Kurz,
Emilio Tuosto
Abstract:
Choreographic approaches to message-passing applications can be regarded as an instance of the model-driven development principles. Choreographies specify interactions among distributed participants coordinating among themselves with message-passing at two levels of abstractions. A global view of the application is specified with a model that abstracts away from asynchrony while a local view of th…
▽ More
Choreographic approaches to message-passing applications can be regarded as an instance of the model-driven development principles. Choreographies specify interactions among distributed participants coordinating among themselves with message-passing at two levels of abstractions. A global view of the application is specified with a model that abstracts away from asynchrony while a local view of the application specifies the communication pattern of each participant. Noteworthy, the latter view can typically be algorithmically obtained by projection of the global view. A crucial element of this approach is to verify the so-called well-formed conditions on global views so that its projections realise a sound communication protocol. We introduce a novel local model, group interface automata, to represent the local view of choreographies and propose a new method to verify the well-formedness of global choreographies. We rely on a recently proposed semantics of global views formalised in terms of pomsets.
△ Less
Submitted 12 September, 2019;
originally announced September 2019.
-
On Resolving Non-determinism in Choreographies
Authors:
Laura Bocchi,
Hernan Melgratti,
Emilio Tuosto
Abstract:
Choreographies specify multiparty interactions via message passing. A realisation of a choreography is a composition of independent processes that behave as specified by the choreography. Existing relations of correctness/completeness between choreographies and realisations are based on models where choices are non-deterministic. Resolving non-deterministic choices into deterministic choices (e.g.…
▽ More
Choreographies specify multiparty interactions via message passing. A realisation of a choreography is a composition of independent processes that behave as specified by the choreography. Existing relations of correctness/completeness between choreographies and realisations are based on models where choices are non-deterministic. Resolving non-deterministic choices into deterministic choices (e.g., conditional statements) is necessary to correctly characterise the relationship between choreographies and their implementations with concrete programming languages. We introduce a notion of realisability for choreographies - called whole-spectrum implementation - where choices are still non-deterministic in choreographies, but are deterministic in their implementations. Our notion of whole spectrum implementation rules out deterministic implementations of roles that, no matter which context they are placed in, will never follow one of the branches of a non-deterministic choice. We give a type discipline for checking whole-spectrum implementations. As a case study, we analyse the POP protocol under the lens of whole-spectrum implementation.
△ Less
Submitted 22 September, 2020; v1 submitted 17 April, 2019;
originally announced April 2019.
-
Tool Supported Analysis of IoT
Authors:
Chiara Bodei,
Pierpaolo Degano,
Letterio Galletta,
Emilio Tuosto
Abstract:
The design of IoT systems could benefit from the combination of two different analyses. We perform a first analysis to approximate how data flow across the system components, while the second analysis checks their communication soundness. We show how the combination of these two analyses yields further benefits hardly achievable by separately using each of them. We exploit two independently devel…
▽ More
The design of IoT systems could benefit from the combination of two different analyses. We perform a first analysis to approximate how data flow across the system components, while the second analysis checks their communication soundness. We show how the combination of these two analyses yields further benefits hardly achievable by separately using each of them. We exploit two independently developed tools for the analyses.
Firstly, we specify IoT systems in IoT-LySa, a simple specification language featuring asynchronous multicast communication of tuples. The values carried by the tuples are drawn from a term-algebra obtained by a parametric signature. The analysis of communication soundness is supported by ChorGram, a tool developed to verify the compatibility of communicating finite-state machines. In order to combine the analyses we implement an encoding of IoT-LySa processes into communicating machines. This encoding is not completely straightforward because IoT-LySa has multicast communications with data, while communication machines are based on point-to-point communications where only finitely many symbols can be exchanged. To highlight the benefits of our approach we appeal to a simple yet illustrative example.
△ Less
Submitted 29 November, 2017;
originally announced November 2017.
-
Reliability and Fault-Tolerance by Choreographic Design
Authors:
Ian Cassar,
Adrian Francalanza,
Claudio Antares Mezzina,
Emilio Tuosto
Abstract:
Distributed programs are hard to get right because they are required to be open, scalable, long-running, and tolerant to faults. In particular, the recent approaches to distributed software based on (micro-)services where different services are developed independently by disparate teams exacerbate the problem. In fact, services are meant to be composed together and run in open context where unpred…
▽ More
Distributed programs are hard to get right because they are required to be open, scalable, long-running, and tolerant to faults. In particular, the recent approaches to distributed software based on (micro-)services where different services are developed independently by disparate teams exacerbate the problem. In fact, services are meant to be composed together and run in open context where unpredictable behaviours can emerge. This makes it necessary to adopt suitable strategies for monitoring the execution and incorporate recovery and adaptation mechanisms so to make distributed programs more flexible and robust. The typical approach that is currently adopted is to embed such mechanisms in the program logic, which makes it hard to extract, compare and debug. We propose an approach that employs formal abstractions for specifying failure recovery and adaptation strategies. Although implementation agnostic, these abstractions would be amenable to algorithmic synthesis of code, monitoring and tests. We consider message-passing programs (a la Erlang, Go, or MPI) that are gaining momentum both in academia and industry. Our research agenda consists of (1) the definition of formal behavioural models encompassing failures, (2) the specification of the relevant properties of adaptation and recovery strategy, (3) the automatic generation of monitoring, recovery, and adaptation logic in target languages of interest.
△ Less
Submitted 23 August, 2017;
originally announced August 2017.
-
Choreographies for Automatic Recovery
Authors:
Claudio Antares Mezzina,
Emilio Tuosto
Abstract:
We propose a choreographic model of reversible computations based on a conservative extension of global graphs and communicating finite-state machines. The main advantage of our approach is that does not require to instrument models in order to control reversibility but for a minor decoration of branches. We show that our models are conservative extensions of existing ones and that the reversible…
▽ More
We propose a choreographic model of reversible computations based on a conservative extension of global graphs and communicating finite-state machines. The main advantage of our approach is that does not require to instrument models in order to control reversibility but for a minor decoration of branches. We show that our models are conservative extensions of existing ones and that the reversible semantics guarantees causal consistency.
△ Less
Submitted 26 May, 2017;
originally announced May 2017.
-
On Sessions and Infinite Data
Authors:
Paula Severi,
Luca Padovani,
Emilio Tuosto,
Mariangiola Dezani-Ciancaglini
Abstract:
We define a novel calculus that combines a call-by-name functional core with session-based communication primitives. We develop a ty** discipline that guarantees both normalisation of expressions and progress of processes and that uncovers an unexpected interplay between evaluation and communication.
We define a novel calculus that combines a call-by-name functional core with session-based communication primitives. We develop a ty** discipline that guarantees both normalisation of expressions and progress of processes and that uncovers an unexpected interplay between evaluation and communication.
△ Less
Submitted 19 June, 2017; v1 submitted 20 October, 2016;
originally announced October 2016.
-
An Abstract Semantics of the Global View of Choreographies
Authors:
Roberto Guanciale,
Emilio Tuosto
Abstract:
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 globa…
▽ More
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.
△ Less
Submitted 10 August, 2016;
originally announced August 2016.
-
Communicating machines as a dynamic binding mechanism of services
Authors:
Ignacio Vissani,
Carlos Gustavo Lopez Pombo,
Emilio Tuosto
Abstract:
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 N…
▽ More
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.
△ Less
Submitted 10 February, 2016;
originally announced February 2016.
-
From Orchestration to Choreography through Contract Automata
Authors:
Davide Basile,
Pierpaolo Degano,
Gian-Luigi Ferrari,
Emilio Tuosto
Abstract:
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 a…
▽ More
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 map** from the contract model to the interaction model, and give conditions to ensure that strong agreement corresponds to well-formed choreography.
△ Less
Submitted 27 October, 2014;
originally announced October 2014.
-
Nominal Regular Expressions for Languages over Infinite Alphabets. Extended Abstract
Authors:
Alexander Kurz,
Tomoyuki Suzuki,
Emilio Tuosto
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, sco** of, and freshness conditions on resources). We discuss classes of such nomi…
▽ More
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, sco** 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.
△ Less
Submitted 26 October, 2013;
originally announced October 2013.
-
On Recovering from Run-time Misbehaviour in ADR
Authors:
Kyriakos Poyias,
Emilio Tuosto
Abstract:
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 fu…
▽ More
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.
△ Less
Submitted 16 October, 2013;
originally announced October 2013.
-
Enforcing Architectural Styles in Presence of Unexpected Distributed Reconfigurations
Authors:
Kyriakos Poyias,
Emilio Tuosto
Abstract:
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 equip** 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 a…
▽ More
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 equip** 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.
△ Less
Submitted 16 December, 2012;
originally announced December 2012.
-
Honesty by Ty**
Authors:
Massimo Bartoletti,
Alceste Scalas,
Emilio Tuosto,
Roberto Zunino
Abstract:
We propose a type system for a calculus of contracting processes. Processes can establish sessions by stipulating contracts, and then can interact either by kee** the promises made, or not. Type safety guarantees that a typeable process is honest - that is, it abides by the contracts it has stipulated in all possible contexts, even in presence of dishonest adversaries. Type inference is decidabl…
▽ More
We propose a type system for a calculus of contracting processes. Processes can establish sessions by stipulating contracts, and then can interact either by kee** the promises made, or not. Type safety guarantees that a typeable process is honest - that is, it abides by the contracts it has stipulated in all possible contexts, even in presence of dishonest adversaries. Type inference is decidable, and it allows to safely approximate the honesty of processes using either synchronous or asynchronous communication.
△ Less
Submitted 27 December, 2016; v1 submitted 12 November, 2012;
originally announced November 2012.
-
Synthesising Choreographies from Local Session Types (extended version)
Authors:
Julien Lange,
Emilio Tuosto
Abstract:
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 ty** systems which allows, under some conditions, to synthesise a choreography (i.e. a multiparty global type) from a set of local session types…
▽ More
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 ty** 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).
△ Less
Submitted 11 April, 2012;
originally announced April 2012.
-
On the realizability of contracts in dishonest systems
Authors:
Massimo Bartoletti,
Emilio Tuosto,
Roberto Zunino
Abstract:
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…
▽ More
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.
△ Less
Submitted 30 January, 2012;
originally announced January 2012.
-
A Modular Toolkit for Distributed Interactions
Authors:
Julien Lange,
Emilio Tuosto
Abstract:
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…
▽ More
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.
△ Less
Submitted 18 October, 2011;
originally announced October 2011.
-
Contracts in distributed systems
Authors:
Massimo Bartoletti,
Emilio Tuosto,
Roberto Zunino
Abstract:
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…
▽ More
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.
△ Less
Submitted 1 August, 2011;
originally announced August 2011.
-
Amending Contracts for Choreographies
Authors:
Laura Bocchi,
Julien Lange,
Emilio Tuosto
Abstract:
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 cri…
▽ More
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.
△ Less
Submitted 1 August, 2011;
originally announced August 2011.
-
Towards Nominal Formal Languages
Authors:
Alexander Kurz,
Tomoyuki Suzuki,
Emilio Tuosto
Abstract:
We introduce formal languages over infinite alphabets where words may contain binders. We define the notions of nominal language, nominal monoid, and nominal regular expressions. Moreover, we extend history-dependent automata (HD-automata) by adding stack, and study the recognisability of nominal languages.
We introduce formal languages over infinite alphabets where words may contain binders. We define the notions of nominal language, nominal monoid, and nominal regular expressions. Moreover, we extend history-dependent automata (HD-automata) by adding stack, and study the recognisability of nominal languages.
△ Less
Submitted 16 February, 2011; v1 submitted 15 February, 2011;
originally announced February 2011.
-
Toward a Formal Semantics for Autonomic Components
Authors:
Marco Aldinucci,
Emilio Tuosto
Abstract:
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 dynam…
▽ More
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.
△ Less
Submitted 2 July, 2010; v1 submitted 13 February, 2010;
originally announced February 2010.
-
Proceedings 2nd Interaction and Concurrency Experience: Structured Interactions
Authors:
Filippo Bonchi,
Davide Grohmann,
Paola Spoletini,
Emilio Tuosto
Abstract:
This volume contains the proceedings of the 2nd Workshop on Interaction and Concurrency Experience (ICE'09). The workshop was held in Bologna, Italy on 31th of August 2009, as a satellite workshop of CONCUR'09. The previous edition of ICE has been organized in Reykjavik (2008).
The ICE workshop is intended as a series of international scientific meetings oriented to researchers in various fiel…
▽ More
This volume contains the proceedings of the 2nd Workshop on Interaction and Concurrency Experience (ICE'09). The workshop was held in Bologna, Italy on 31th of August 2009, as a satellite workshop of CONCUR'09. The previous edition of ICE has been organized in Reykjavik (2008).
The ICE workshop is intended as a series of international scientific meetings oriented to researchers in various fields of theoretical computer science and, each year, the workshop focuses on a specific topic: ICE 2009 focused on structured interactions meant as the class of synchronisations that go beyond the "simple" point-to-point synchronisations (e.g., multicast or broadcast synchronisations, even-notification based interactions, time dependent interactions, distributed transactions,...).
△ Less
Submitted 3 December, 2009;
originally announced December 2009.
-
Heuristic Methods for Security Protocols
Authors:
Qurat ul Ain Nizamani,
Emilio Tuosto
Abstract:
Model checking is an automatic verification technique to verify hardware and software systems. However it suffers from state-space explosion problem. In this paper we address this problem in the context of cryptographic protocols by proposing a security property-dependent heuristic. The heuristic weights the state space by exploiting the security formulae; the weights may then be used to explore…
▽ More
Model checking is an automatic verification technique to verify hardware and software systems. However it suffers from state-space explosion problem. In this paper we address this problem in the context of cryptographic protocols by proposing a security property-dependent heuristic. The heuristic weights the state space by exploiting the security formulae; the weights may then be used to explore the state space when searching for attacks.
△ Less
Submitted 21 October, 2009;
originally announced October 2009.
