Swarm protocols are a recently introduced formalism for specifying, implementing, and verifying peer-to-peer systems called swarms. A swarm consists of distributed agents called machines that communicate by asynchronous event propagation. Following a local-first model, each machine can progress without requiring continuous connectivity to other machines. Existing models of swarms are not compositional, making the modular development of large and complex swarm applications as well as the reuse of code difficult. We address these issues by presenting novel theory and techniques for the compositional specification, verification, and implementation of swarms. These results enable the correct compositional reuse of pre-existing swarm protocols and machine implementations. We implement these contributions in a companion software artifact which enables the automatic integration of independently designed and verified swarm components.

We propose a formal approach for specifying and implementing decentralised coordination in distributed systems, with a focus on smart contracts. Our model captures dynamic roles, data-driven transitions, and external coordination interfaces, enabling high-level reasoning about decentralised workflows. We implement a toolchain that supports formal model validation, code generation for Solidity (our framework is extendable to other smart contract languages), and automated test synthesis. Although our implementation targets blockchain platforms, the methodology is platform-agnostic and may generalise to other service-oriented and distributed architectures. We demonstrate the expressiveness and practicality of the approach by modelling and realising some coordination patterns in smart contracts.

We present MoCheQoS , a bounded mo del che cker to statically analyse Quality of Service ( QoS ) properties of message-passing systems. The tool implements a theoretical framework for compositional analysis of QoS properties across distributed systems using QoS-extended communicating finite state machines (qCFSMs) and the dynamic temporal logic QL with choreography-indexed modalities. To achieve this, MoCheQoS integrates Z3 SMT solver for constraint verification and ChorGram for choreographic model processing. Our methodology enables systematic verification of QoS properties on measurable application-level attributes and resource consumption metrics (e.g., monetary cost, execution time, memory usage) through bounded model checking with user-specified run length limits.

Join patterns provide a promising approach to the development of concurrent and distributed message-passing applications. Several variations and implementations have been presented in the literature - but various aspects remain under-explored: in particular, how to specify a suitable notion of message matching, how to implement it correctly and efficiently, and how to systematically evaluate the implementation performance. In this work we focus on actor-based programming, and study the application of join patterns with conditional guards (i.e., the most expressive and challenging version of join patterns in literature). We formalise a novel specification of fair and deterministic join pattern matching, ensuring that older messages are always consumed if they can be matched. We present a stateful, tree-based join pattern matching algorithm and prove that it correctly implements our fair and deterministic matching specification. We present a novel Scala 3 actor library (called JoinActors) that implements our join pattern formalisation, leveraging macros to provide an intuitive API. Finally, we evaluate the performance of our implementation, by introducing a systematic benchmarking approach that takes into account the nuances of join pattern matching (in particular, its sensitivity to input traffic and complexity of patterns and guards).

Abstract We present "Image missing", a bounded "Image missing""Image missing"to statically analyse Quality of Service ( "Image missing") properties of message-passing systems. 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 applicability of "Image missing"is evaluated through case studies and experiments. A first case study is based on the AWS cloud while a second one analyses a communicating system automatically extracted from code. Additionally, we consider synthetically generated experiments to assess the scalability of "Image missing". These experiments showed that our model can faithfully capture and effectively analyse QoS properties in industrial-strength scenarios.

Abstract Data races are a particular kind of subtle, unintended program behaviour arising from thread interference in shared-memory concurrency. In this paper, we propose an automated technique for static detection of data races in multi-threaded C programs with POSIX threads. The key element of our technique is a reduction to reachability. Our prototype implementation combines such reduction with context-bounded analysis. The approach proves competitive against state-of-the-art tools, finding new issues in the implementation of well-known lock-free data structures, and shows a considerably superior accuracy of analysis in the presence of complex shared-memory access patterns.

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.

Abstract Non-functional properties of collective adaptive systems (CAS) are of paramount relevance practically in any application. This paper compares two recently proposed approaches to quantitative modelling that exploit different system abstractions: the first is based on generalised stochastic Petri nets, and the second is based on queueing networks. Through a case study involving autonomous robots, we analyse and discuss the relative merits of the approaches. This is done by considering three scenarios which differ on the architecture used to coordinate the distributed components. Our experimental results assess a high accuracy when comparing model-based performance analysis results derived from two different quantitative abstractions for CAS.

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.

Abstract We sketch a sequentialization-based technique for bounded detection of data races under sequential consistency, and summarise the major improvements to our verification framework over the last years.

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, which are 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 choreographies and their admissible refinements in terms of an axiom scheme.

International audience

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.

We define a novel calculus that combines a call-by-name functional core with session-based communication primitives. We develop a typing 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 typing discipline that guarantees both normalisation of expressions and progress of processes and that uncovers an unexpected interplay between evaluation and communication. Comment: 39 pages 6 files including .bbl

We report on the analysis of gen_server, a popular Erlang library to build client-server applications. Our analysis uses a tool based on choreographic models. We discuss how, once the library has been modelled in terms of communicating finite state machines, an automated analysis can be used to detect potential communication errors. The results of our analysis suggest how to properly use gen_server in order to guarantee the absence of communication errors.

Graphical choreographies, or global graphs, are general multiparty session specifications featuring expressive constructs such as forking, merging, and joining for representing application-level protocols. Global graphs can be directly translated into modelling notations such as BPMN and UML. This paper presents an algorithm whereby a global graph can be constructed from asynchronous interactions represented by communicating finite-state machines (CFSMs). Our results include: a sound and complete characterisation of a subset of safe CFSMs from which global graphs can be constructed; an algorithm to translate CFSMs to global graphs; a time complexity analysis; and an implementation of our theory, as well as an experimental evaluation.

We present a theory for the design and verification of distributed transactions in dynamically reconfigurable systems. Despite several formal approaches have been proposed to study distributed transactional behaviours, the inter-relations between failure propagation and dynamic system reconfiguration still need investigation. We propose a formal model for transactions in service oriented architectures (SOAs) inspired by the attribute mechanisms of the Java Transaction API. Technically, we model services in ATc (after ‘Attribute-basedTransactionalcalculus’), a CCS-like process calculus where service declarations are decorated with atransactional attribute. Such attribute disciplines, upon service invocation, how the invoked service is executed with respect to the transactional scopes of the invoker. A type system ensures that well-typed ATc systems do not exhibit run-time errors due to misuse of the transactional mechanisms. Finally, we define a testing framework for distributed transactions in SOAs based on ATc and prove that under reasonable conditions some attributes are observationally indistinguishable.

Ambient-PRISMA is an architectural approach for specifying aspect-oriented software architecture and generating code of distributed and mobile systems. Ambient-PRISMA lacks a precise semantics due to the fact that it is based only on a metamodel. In this paper, Ambient-PRISMA is mapped into a formal language called Channel Ambient Calculus, a process algebra for specifying mobile applications that provides channels and ambients as first-class citizens. We argue that the formalization in Channel Ambient Calculus is particularly well-suited for modelling Ambient-PRISMA.

We present SHReQ, a formal framework for specifying systems that handle abstract high-level QoS requirements which are becoming more and more important for service oriented computing. SHReQ combines synchronised hyperedge replacement (SHR) with constraint-semirings. SHR is a (hyper)graph rewriting mechanism for modelling evolution of systems. The novelty of the approach relies on the synchronisation mechanism which is based on constraint-semirings, algebraic structures that provide both the mathematics for multi-criteria QoS and the synchronisation policies underlying the SHR mechanism.