Abstract
We present a machine-checked proof of security for the domain management protocol of Amazon Web Services' KMS (Key Management Service) a critical security service used throughout AWS and by AWS customers. Domain management is at the core of AWS KMS; it governs the top-level keys that anchor the security of encryption services at AWS. We show that the protocol securely implements an ideal distributed encryption mechanism under standard cryptographic assumptions. The proof is machine-checked in the EasyCrypt proof assistant and is the largest EasyCrypt development to date.

Abstract
Rapidly changing customer demands, regulations and technologies drive the complexity of products, processes and production systems, as well as shorter product and factory lifecycles. In order to handle such complexity while decreasing the time-to-market, immersive virtual reality (VR) technologies are increasingly being used in industry to support product and factory lifecycle engineering processes, such as (re)design, validation and verification, learning and training. However, the design and development of multi-user VR training for complex and manual production processes remain a challenge for industry. The integration of VR training simulations with virtual and physical factories could support the handling of such obstacles in terms of efficiency and effectiveness by increasing the precision, accuracy and reliability of data used in VR simulations. In this study, we present a collaborative and coordinated VR training model and its data integration with virtual factory tools and manufacturing execution systems for a wind turbine assembly scenario. A demonstration has been performed and evaluated by industry experts. The preliminary evaluation results show that integrated collaborative VR training has significant potential for more efficient and effective training, as well as enabling new use cases for industry.

Abstract
The energy requirements of thruster driven autonomous underwater vehicle (AUV) missions have been growing in recent years. Their complexity and length are continuously increasing due to the growth of undersea exploration. The use of variable buoyancy systems (VBS) can potentially lead to energy savings since consumption is only required for buoyancy changes. As such, energy is only spent during limited periods of time, as opposed to thruster driven systems, where consumption is typically continuous. In this work, an energetic comparison between thruster and VBS driven devices is performed for a specific mission profile and a defined set of parameters. The influence of the mission parameters is studied in order to determine which system leads to the lowest energy consumption. For the case study presented, it is shown that the use of VBS over thrusters can lead to considerable energetic savings. © 2019 IEEE.

Abstract
We propose (formula presented) -logic as a formal foundation for the specification and development of event-based systems with local data states. The logic is intended to cover a broad range of abstraction levels from abstract requirements specifications up to constructive specifications. Our logic uses diamond and box modalities over structured actions adopted from dynamic logic. Atomic actions are pairs where e is an event and (formula presented) a state transition predicate capturing the allowed reactions to the event. To write concrete specifications of recursive process structures we integrate (control) state variables and binders of hybrid logic. The semantic interpretation relies on event/data transition systems; specification refinement is defined by model class inclusion. For the presentation of constructive specifications we propose operational event/data specifications allowing for familiar, diagrammatic representations by state transition graphs. We show that (formula presented) -logic is powerful enough to characterise the semantics of an operational specification by a single (formula presented) -sentence. Thus the whole development process can rely on (formula presented) -logic and its semantics as a common basis. This includes also a variety of implementation constructors to support, among others, event refinement and parallel composition. © The Author(s) 2019.

Abstract
This paper proposes the implementation of a framework for the development of collaborative extended reality (XR) applications. Using the framework, developers can focus on understanding which collaborative mechanisms they need to implement for the respective reality model application. In this paper we specifically study collaborative mechanisms around object manipulation in Virtual Reality (VR). As such, we planned a VR prototype using the proposed framework, which was used to validate the various interaction and collaboration features in VR. The gathered data from the user tests revealed that they enjoyed the experience and the collaborative mechanisms helped them work together. Furthermore, to understand whether the framework allowed for the development of XR applications, we decided to implement an augmented reality prototype as well. Afterwards, we ran an experiment with 4 VR and 3 AR users sharing the same virtual environment. The experiment was successful at allowing them to interact in real-time in the same shared environment. Therefore, the framework enables the development of XR applications that support different mixed-reality technologies.

Abstract
Design complexity and its relation to Design for Manufacturing continues to be a challenging topic, namely when the objective is to address these aspects in a straightforward manner to young or less experienced design teams. The availability of practical methodologies that induce rules to support novel design creation, in the environment of manufacturing processes, continues to be scarce. This work presents a novel approach named - 0-3D Design Method - that aims to define, in a systematic and geometrical manner, practical rules that allows mechanical designers to relate, in a codified manner, the design geometry of a given mechanical component to the typical manufacturing processes that permit its physical embodiment. The method proposes the definition of types and sub-types of parts, based on the number of spatial dimensions that need to be modified for a given design construction, and its relation to the manufacturing phase of the product life-cycle. A practical mechanical design example is presented to demonstrate the methodology, mapping the parts necessary for the design of a cutting head of a machine-tool. (C) 2019 The Authors. Published by Elsevier B.V.