Abstract

Abstract
Construction and analysis of distributed systems is difficult. Multiparty session types (MPST) constitute a method to make it easier. The idea is to use type checking to statically prove deadlock freedom and protocol compliance of communicating processes. In practice, the premier approach to apply the MPST method in combination with mainstream programming languages has been based on API generation. In this paper (pearl), we revisit and revise this approach. Regarding our “revisitation”, using Scala 3, we present the existing API generation approach, which is based on deterministic finite automata (DFA), in terms of both the existing states-as-classes encoding of DFAs as APIs, and a new states-as-type-parameters encoding; the latter leverages match types in Scala 3. Regarding our “revision”, also using Scala 3, we present a new API generation approach that is based on sets of pomsets instead of DFAs; it crucially leverages match types, too. Our fresh perspective allows us to avoid two forms of combinatorial explosion resulting from implementing concurrent subprotocols in the DFA-based approach. We implement our approach in a new API generation tool. © Guillermina Cledou, Luc Edixhoven, Sung-Shik Jongmans, and Jos Proena; licensed under Creative Commons License CC-BY 4.0

Abstract

Abstract
Multiparty session types (MPST) constitute a method to simplify construction and analysis of distributed systems. The idea is that well-typedness of processes at compile-time (statically) entails deadlock freedom and protocol compliance of their sessions of communications at execution-time (dynamically). In practice, the premier approach to apply the MPST method in combination with mainstream programming languages has been based on API generation. However, existing MPST tools support only unilingual programming (homogeneity), while many real-world distributed systems are engineered using multilingual programming (heterogeneity). In this paper, we present a blueprint of ST4MP: a tool to apply the MPST method in multilingual programming, based on API generation. © 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Abstract
The complexity of systems continues to increase rapidly, especially due to the multi-level integration of subsystems from different domains into cyber-physical systems. This results in special challenges for the efficient verification and validation (V&V) of these systems with regard to their requirements and properties. In order to tackle the new challenges and improve the quality assurance processes, the V&V workflows have to be documented and analyzed. In this paper, a novel approach for the workflow modelling of V&V activities is presented. The generic approach is tailorable to different industrial domains and their specific constraints, V&V methods, and toolchains. The outcomes comprise a dedicated modelling notation (VVML) and tool-support using the modelling framework Enterprise Architect for the efficient documentation and implementation of workflows in the use cases. The solution enables the design of re-usable workflow assets such as V&V activities and artifacts that are exchanged between workflows. This work is part of the large scale European research project VALU3S that deals with the improvement and evaluation of V&V processes in different technical domains, focusing on safety, cybersecurity, and privacy properties.

Abstract