Search

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., Comment: This preprint is the author version of the paper published at COORDINATION 2024

This paper explores the problem of determining which classes of Petri nets can be encoded into behaviourally-equivalent CCS processes. Most of the existing related literature focuses on the inverse problem (i.e., encoding process calculi belonging to the CCS family into Petri nets), or extends CCS with Petri net-like multi-synchronisation (Multi-CCS). In this work, our main focus are free-choice and workflow nets (which are widely used in process mining to describe system interactions) and our target is plain CCS. We present several novel encodings, including one from free-choice workflow nets (produced by process mining algorithms like the alpha-miner) into CCS processes, and we prove that our encodings produce CCS processes that are weakly bisimilar to the original net. Besides contributing new expressiveness results, our encodings open a door towards bringing analysis and verification techniques from the realm of process calculi into the realm of process mining., Comment: 38 pages, 18 figures, extended version of paper to be published at COORDINATION 2024

Behavioural types provide a promising way to achieve lightweight, language-integrated verification for communication-centric software. However, a large barrier to the adoption of behavioural types is that the current state of the art expects software to be written using the same tools and typing discipline throughout a system, and has little support for components over which a developer has no control. This position paper describes the outcomes of a working group discussion at Dagstuhl Seminar 24051 (Next-Generation Protocols for Heterogeneous Systems). We propose a methodology for integrating multiple behaviourally-typed components, written in different languages. Our proposed approach involves an extensible protocol description language, a session IR that can describe data transformations and boundary monitoring and which can be compiled into program-specific session proxies, and finally a session middleware to aid session establishment. We hope that this position paper will stimulate discussion on one of the most pressing challenges facing the widespread adoption of behavioural typing., Comment: In Proceedings PLACES 2024, arXiv:2404.03712

Software-Defined Networking (SDN) significantly simplifies programming, reconfiguring, and optimizing network devices, such as switches and routers. The de facto standard for programmming SDN devices is the P4 language. However, the flexibility and power of P4, and SDN more generally, gives rise to important risks. As a number of incidents at major cloud providers have shown, errors in SDN programs can compromise the availability of networks, leaving them in a non-functional state. The focus of this paper are errors in control-plane programs that interact with P4-enabled network devices via the standardized P4Runtime API. For clients of the P4Runtime API it is easy to make mistakes that lead to catastrophic failures, despite the use of Google's Protocol Buffers as an interface definition language. This paper proposes P4R-Type, a novel verified P4Runtime API for Scala that performs static checks for P4 control plane operations, ruling out mismatches between P4 tables, allowed actions, and action parameters. As a formal foundation of P4R-Type, we present the $F_{\text{P4R}}$ calculus and its typing system, which ensure that well-typed programs never get stuck by issuing invalid P4Runtime operations. We evaluate the safety and flexibility of P4R-Type with 3 case studies. To the best of our knowledge, this is the first work that formalises P4Runtime control plane applications, and a typing discipline ensuring the correctness of P4Runtime operations., Comment: 82 pages, 27 figures, extended version of paper to be published at OOPSLA 2023

This volume contains the proceedings of PLACES 2023, the 14th edition of the Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software. The PLACES workshop series offers a forum for researchers from different fields to exchange new ideas about the challenges of modern and future programming, where concurrency and distribution are the norm rather than a marginal concern. PLACES 2023 was held on 22 April 2023 in Paris, France. The programme included keynote talks by Marieke Huisman and Vasco T. Vasconcelos, presentations of five research papers, and six talks about preliminary or already-published work that could foster interesting discussion during the workshop. These proceedings contain the five accepted research papers, the abstracts of the keynote talks, and a list of the other contributions.

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., Comment: SI: Special Issue on Selected Tool Papers of the 22nd and 23rd International Conference on Coordination Models and Languages, COORDINATION 2020 and 2021

This volume contains the proceedings of ICE'22, the 15th Interaction and Concurrency Experience, which was held as an hybrid event in Lucca, Italy, and as a satellite event of DisCoTec'22. The ICE workshop series features a distinguishing review and selection procedure: PC members are encouraged to interact, anonymously, with authors. The 2022 edition of ICE included double blind reviewing of original research papers, in order to increase fairness and avoid bias in reviewing. Each paper was reviewed by between two and four PC members (with an average of 3.33333333333), and altogether 5 papers were accepted for publication -- plus 3 oral presentations which are not part of this volume. We were proud to host 2 invited talks, by Ilaria Castellani and Matthew Parkinson. The abstracts of these talks are included in this volume, together with the final versions of the research papers, which take into account the discussion at the workshop.

Session types enable the specification and verification of communicating systems. However, their theory often assumes that processes never fail. To address this limitation, we present a generalised multiparty session type (MPST) theory with crash-stop failures, where processes can crash arbitrarily. Our new theory validates more protocols and processes w.r.t. previous work. We apply minimal syntactic changes to standard session {\pi}-calculus and types: we model crashes and their handling semantically, with a generalised MPST typing system parametric on a behavioural safety property. We cover the spectrum between fully reliable and fully unreliable sessions, via optional reliability assumptions, and prove type safety and protocol conformance in the presence of crash-stop failures. Introducing crash-stop failures has non-trivial consequences: writing correct processes that handle all crash scenarios can be difficult. Yet, our generalised MPST theory allows us to tame this complexity, via model checking, to validate whether a multiparty session satisfies desired behavioural properties, e.g. deadlock-freedom or liveness, even in presence of crashes. We implement our approach using the mCRL2 model checker, and evaluate it with examples extended from the literature., Comment: Extended version of paper accepted at CONCUR 2022. This version fixes a missing condition in fairness

This volume contains the proceedings of ICE'21, the 14th Interaction and Concurrency Experience, which was held online on the 18th of June 2021, as a satellite event of DisCoTec'21. The ICE workshop series features a distinguishing review and selection procedure, allowing PC members to interact anonymously with authors. As in the past 13 editions, this interaction considerably improved the accuracy of the feedback from the reviewers and the quality of accepted papers, and offered the basis for lively discussion during the workshop. The 2021 edition of ICE included double blind reviewing of original research papers, in order to increase fairness and avoid bias in reviewing. Each paper was reviewed by three or four PC members, and altogether 5 papers were accepted for publication - plus 4 oral presentations which are not part of this volume. We were proud to host 2 invited talks, by Laura Bocchi and Helene Coullon. The abstracts of these talks are included in this volume together with the regular papers. The final versions of the contributions, taking into account the discussion at the workshop, are included.

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.

In concurrent and distributed systems, software components are expected to communicate according to predetermined protocols and APIs - and if a component does not observe them, the system's reliability is compromised. Furthermore, isolating and fixing protocol/API errors can be very difficult. Many methods have been proposed to check the correctness of communicating systems, ranging from compile-time to run-time verification; among such methods, session types have been applied for both static type-checking, and run-time monitoring. This work takes a fresh look at the run-time verification of communicating systems using session types, in theory and in practice. On the theoretical side, we develop a novel formal model of session-monitored processes; with it, we formulate and prove new results on the monitorability of session types, connecting their run-time and static verification - in terms of soundness (i.e., whether monitors only flag ill-typed processes) and completeness (i.e., whether all ill-typed processes can be flagged by a monitor). On the practical side, we show that our monitoring theory is indeed realisable: building upon our formal model, we develop a Scala toolkit for the automatic generation of session monitors. Our executable monitors can be used to instrument black-box processes written in any programming language; we assess the viability of our approach with a series of benchmarks.

This paper presents the first formalisation of the precise subtyping relation for asynchronous multiparty sessions. We show that our subtyping relation is sound (i.e., guarantees safe process replacement) and also complete: any extension of the relation is unsound. To achieve our results, we develop a novel session decomposition technique, from full session types (including internal/external choices) into single input/output session trees (without choices). Previous work studies precise subtyping for binary sessions (with just two participants), or multiparty sessions (with any number of participants) and synchronous interaction. Here, we cover multiparty sessions with asynchronous interaction, where messages are transmitted via FIFO queues (as in the TCP/IP protocol), and prove that our subtyping is both operationally and denotationally precise. In the asynchronous multiparty setting, finding the precise subtyping relation is a highly complex task: this is because, under some conditions, participants can permute the order of their inputs and outputs, by sending some messages earlier or receiving some later, without causing errors; the precise subtyping relation must capture all such valid permutations -- and consequently, its formalisation, reasoning and proofs become challenging. Our session decomposition technique overcomes this complexity, expressing the subtyping relation as a composition of refinement relations between single input/output trees, and providing a simple reasoning principle for asynchronous message optimisations.

We develop a formal model of Algorand stateless smart contracts (stateless ASC1.) We exploit our model to prove fundamental properties of the Algorand blockchain, and to establish the security of some archetypal smart contracts. While doing this, we highlight various design patterns supported by Algorand. We perform experiments to validate the coherence of our formal model w.r.t. the actual implementation.

This volume contains the proceedings of ICE'20, the 13th Interaction and Concurrency Experience, which was held online on the 19th of June 2020, as a satellite event of DisCoTec'20. The ICE workshop series features a distinguishing review and selection procedure, allowing PC members to interact anonymously with authors. As in the past 12 editions, this interaction considerably improved the accuracy of the feedback from the reviewers and the quality of accepted papers, and offered the basis for lively discussion during the workshop. The 2020 edition of ICE included double blind reviewing of original research papers, in order to increase fairness and avoid bias in reviewing. Each paper was reviewed by three PC members, and altogether 5 papers were accepted for publication - plus 5 oral presentations which are not part of this volume. We were proud to host 2 invited talks, by Cinzia Di Giusto and Karoliina Lehtinen. The abstracts of these talks are included in this volume together with the regular papers. The final versions of the contributions, taking into account the discussion at the workshop, are included.

This volume contains the proceedings of ICE'19, the 12th Interaction and Concurrency Experience, which was held in Copenhagen, Denmark on the 20th and 21st of June 2019, as a satellite event of DisCoTec'19. The ICE workshop series features a distinguishing review and selection procedure, allowing PC members to interact anonymously with authors. As in the past 11 editions, this interaction considerably improved the accuracy of the feedback from the reviewers and the quality of accepted papers, and offered the basis for lively discussion during the workshop. The 2019 edition of ICE included double blind reviewing of original research papers, in order to increase fairness and avoid bias in reviewing. Each paper was reviewed by three PC members, and altogether 9 papers were accepted for publication - plus 2 oral presentations which are not part of this volume. We were proud to host 4 invited talks, by Dilian Gurov, Fritz Henglein, Sophia Knight, and Hern\'an Melgratti. The abstracts of these talks are included in this volume together with the regular papers. Final versions of the contributions, taking into account the discussion at the workshop, are included.

Multiparty Session Types (MPST) are a well-established typing discipline for message-passing processes interacting on sessions involving two or more participants. Session typing can ensure desirable properties: absence of communication errors and deadlocks, and protocol conformance. However, existing MPST works provide a subject reduction result that is arguably (and sometimes, surprisingly) restrictive: it only holds for typing contexts with strong duality constraints on the interactions between pairs of participants. Consequently, many "intuitively correct" examples cannot be typed and/or cannot be proved type-safe. We illustrate some of these examples, and discuss the reason for these limitations. Then, we outline a novel MPST typing system that removes these restrictions., Comment: In Proceedings PLACES 2017, arXiv:1704.02418

Subtyping in concurrency has been extensively studied since early 1990s as one of the most interesting issues in type theory. The correctness of subtyping relations has been usually provided as the soundness for type safety. The converse direction, the completeness, has been largely ignored in spite of its usefulness to define the largest subtyping relation ensuring type safety. This paper formalises preciseness (i.e. both soundness and completeness) of subtyping for mobile processes and studies it for the synchronous and the asynchronous session calculi. We first prove that the well-known session subtyping, the branching-selection subtyping, is sound and complete for the synchronous calculus. Next we show that in the asynchronous calculus, this subtyping is incomplete for type-safety: that is, there exist session types T and S such that T can safely be considered as a subtype of S, but T < S is not derivable by the subtyping. We then propose an asynchronous subtyping system which is sound and complete for the asynchronous calculus. The method gives a general guidance to design rigorous channel-based subtypings respecting desired safety properties. Both the synchronous and the asynchronous calculus are first considered with lin ear channels only, and then they are extended with session initialisations and c ommunications of expressions (including shared channels).

Labelled Transition Systems (LTSs) are a fundamental semantic model in many areas of informatics, especially concurrency theory. Yet, reasoning on LTSs and relations between their states can be difficult and elusive: very simple process algebra terms can give rise to a large (possibly infinite) number of intricate transitions and interactions. To ease this kind of study, we present LTSwb, a flexible and extensible LTS toolbox: this tutorial paper discusses its design and functionalities., Comment: In Proceedings ICE 2015, arXiv:1508.04595

We propose a formal model for distributed systems, where each participant advertises its requirements and obligations as behavioural contracts, and where multiparty sessions are started when a set of contracts allows to synthesise a choreography. Our framework is based on the CO2 calculus for contract-oriented computing, and borrows concepts and results from the session type literature. It supports sessions where the number of participants is not determined beforehand, and keeps CO2's ability to rule out participants that are culpable if contracts are not fulfilled at runtime. We show that we have progress and session fidelity in CO2, as a result of the honesty of participants - i.e., their ability to always adhere to their contracts., Comment: In Proceedings ICE 2013, arXiv:1310.4019

We propose a type system for a calculus of contracting processes. Processes can establish sessions by stipulating contracts, and then can interact either by keeping 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.