Abstract
[No abstract available]

Abstract
Manufacturers of automated systems and their components have been allocating an enormous amount of time and effort in R&D activities, which led to the availability of prototypes demonstrating new capabilities as well as the introduction of such systems to the market within different domains. Manufacturers need to make sure that the systems function in the intended way and according to specifications. This is not a trivial task as system complexity rises dramatically the more integrated and interconnected these systems become with the addition of automated functionality and features to them. This effort translates into an overhead on the V&V (verification and validation) process making it time-consuming and costly. In this paper, we present VALU3S, an ECSEL JU (joint undertaking) project that aims to evaluate the state-of-the-art V&V methods and tools, and design a multi-domain framework to create a clear structure around the components and elements needed to conduct the V&V process. The main expected benefit of the framework is to reduce time and cost needed to verify and validate automated systems with respect to safety, cyber-security, and privacy requirements. This is done through identification and classification of evaluation methods, tools, environments and concepts for V&V of automated systems with respect to the mentioned requirements. VALU3S will provide guidelines to the V&V community including engineers and researchers on how the V&V of automated systems could be improved considering the cost, time and effort of conducting V&V processes. To this end, VALU3S brings together a consortium with partners from 10 different countries, amounting to a mix of 25 industrial partners, 6 leading research institutes, and 10 universities to reach the project goal. © 2021 The Authors

Abstract
Background: modern robots employ artificial intelligence algorithms in a broad ange of applications. These robots acquire information about their surroundings and use these highly-specialized algorithms to reason about their next actions. Despite their effectiveness, artificial intelligence algorithms are highly susceptible to adversarial attacks. This work focuses on mitigating attacks aimed at tampering with the communication channel between nodes running micro-ROS, which is an adaptation of the Robot Operating System (ROS) for extremely resource-constrained devices (usually assigned to collect information), and more robust nodes running ROS2, typically in charge of executing computationally costly tasks, like processing artificial intelligence algorithms. Methods: we followed the instructions described in the Data Distribution Service for Extremely Resource Constrained Environments (DDS-XRCE) specification on how to secure the communication between micro-ROS and ROS2 nodes and developed a custom communication transport that combines the application programming interface (API) provided by eProsima and the implementation of the Transport Security Layer version 1.3 (TLS 1.3) protocol developed by wolfSSL. Results: first, we present the first open-source transport layer based on TLS 1.3 to secure the communication between micro-ROS and ROS2 nodes, providing initial benchmarks that measure its temporal overhead. Second, we demystify how the DDS-XRCE and DDS Security specifications interact from a cybersecurity point of view. Conclusions: by providing a custom encrypted transport for micro-ROS and ROS2 applications to communicate, extremely resource-constrained devices can now participate in DDS environments without compromising the security, privacy, and authenticity of their message exchanges with ROS2 nodes. Initial benchmarks show that encrypted single-value messages present around 20% time overhead compared to the default non-encrypted micro-ROS transport. Finally, we presented an analysis of how the DDS-XRCE and DDS Security specifications relate to each other, providing insights not present in the literature that are crucial for further investigating the security characteristics of combining these specifications.

Abstract
Choreographic languages describe possible sequences of interactions among a set of agents. Typical models are based on languages or automata over sending and receiving actions. Pomsets provide a more compact alternative by using a partial order to explicitly represent causality and concurrency between these actions. However, pomsets offer no representation of choices, thus a set of pomsets is required to represent branching behaviour. For example, if an agent Alice can send one of two possible messages to Bob three times, one would need a set of 2 x 2 x 2 distinct pomsets to represent all possible branches of Alice's behaviour. This paper proposes an extension of pomsets, named branching pomsets, with a branching structure that can represent Alice's behaviour using 2 + 2 + 2 ordered actions. We compare the expressiveness of branching pomsets with that of several forms of event structures from the literature. We encode choreographies as branching pomsets and show that the pomset semantics of the encoded choreographies are bisimilar to their operational semantics. Furthermore, we define well-formedness conditions on branching pomsets, inspired by multiparty session types, and we prove that the well-formedness of a branching pomset is a sufficient condition for the realisability of the represented com-munication protocol. Finally, we present a prototype tool that implements our theory of branching pomsets, focusing on its applications to choreographies. (c) 2023 The Author(s). Published by Elsevier Inc. This is an open access article under the CC BY license (http://creativecommons .org /licenses /by /4 .0/).

Abstract

Abstract
This tool paper presents Caos: a methodology and a programming framework for computer-aided design of structural operational semantics for formal models. This framework includes a set of Scala libraries and a workflow to produce visual and interactive diagrams that animate and provide insights over the structure and the semantics of a given abstract model with operational rules. Caos follows an approach in which theoretical foundations and a practical tool are built together, as an alternative to foundations-first design (tool justifies theory) or tool-first design (foundations justify practice). The advantage of Caos is that the tool-under-development can immediately be used to automatically run numerous and sizeable examples in order to identify subtle mistakes, unexpected outcomes, and unforeseen limitations in the foundations-under-development, as early as possible. We share two success stories of Caos' methodology and framework in our own teaching and research context, where we analyse a simple while-language and a choreographic language, including their operational rules and the concurrent composition of such rules. We further discuss how others can include Caos in their own analysis and Scala tools.