Abstract
Virtual reality (VR) has the potential to significantly boost productivity in professional settings, especially those that can benefit from immersive environments that allow a better and more thorough way of visualizing information. However, the physical demands of mid-air movements make it difficult to use VR for extended periods. DeskVR offers a solution that allows users to engage in VR while seated at a desk, minimizing physical exhaustion. However, developing appropriate motion techniques for this context is challenging due to limited mobility and space constraints. This work focuses on object manipulation techniques, exploring touch-based and mid-air-based approaches to design a suitable solution for DeskVR, hypothesizing that touch-based object manipulation techniques could be as effective as mid-air object manipulation in a DeskVR scenario while less physically demanding. Thus, we propose Scaled Indirect Touch 6-DOF (SIT6), an indirect touch-based object manipulation technique incorporating scaled input mapping to address precision and out-of-reach manipulation issues. The implementation of our solution consists of a state machine with error-handling mechanisms and visual indicators to enhance interaction. User experiments were conducted to compare the SIT6 technique with a baseline mid-air approach, revealing comparable effectiveness while demanding less physical exertion. These results validated our hypothesis and established SIT6 as a viable option for object manipulation in DeskVR scenarios. (c) 2023 The Authors. Published by Elsevier Ltd. This is an open access article under the CC BY license (http://creativecommons.org/licenses/by/4.0/).

Abstract
Designing systems to serve a large number of people, who have similar demands, but also have varied needs and generate a huge volume of data, requires a software architecture that allows constant evolution, is easy to maintain, and has the ability to scale smartly. The SPL technique with microservices architecture seems promising to meet these requirements, but this integration is not trivial. Thus, we conduct a SLR that identified 3 architectures that proposed the combination of these techniques. However, the architectures found were complex and reduced time-to-market, as they proposed the implementation of all resources through microservices. Thus, in order to reduce the complexity of development and, consequently, reduce the time to market, this work presents a proposal for the design of a hybrid SPL architecture, through the combination of large backend APIs and microservices. In addition, this research paper presents a case study that consisted of defining the architecture of a medical clinics SPL as a Multi-tenant Software as a Service. Finally, we compare the complexity of the architecture generated using our approach, with a microservice architecture constructed using other approach found in literature.

Abstract

Abstract
With the incresasing importance of program verification, an issue that has been receiving more attention is the certification of verification tools, addressing the vernacular question: Who verifies the verifier?. In this paper we approach this meta-verification problem by focusing on a fundamental component of program verifiers: the Verification Conditions Generator (VCGen), responsible for producing a set of proof obligations from a program and a specification. The semantic foundations of VCGens lie in program logics, such as Hoare logic, Dynamic logic, or Separation logic, and related predicate transformers. Dynamic logic is the basis of the KeY system, one of the foremost deductive verifiers, whose logic makes use of the notion of update, which is quite intricate to formalize. In this paper we derive systematically, based on a KeY-style dynamic logic, a correct-by-construction VCGen for a toy programming language. Our workflow covers the entire process, from the logic to the VCGen. It is implemented in the Why3 tool, which is itself a program verifier. We prove the soundness and (an appropriate notion of) completeness of the logic, then define a VCGen for our language and establish its soundness. Dynamic logic is one of a variety of research topics that our dear friend and colleague Luis Soares Barbosa has, over the years, initiated and promoted at the University of Minho. It is a pleasure for us to dedicate this work to him on the occasion of his 60th birthday.

Abstract

Abstract
Currently, distributed software systems have evolved at an unprecedented pace. Modern software-quality requirements are high and require significant staff support and effort. This study investigates the use of a supervised machine learning model, a Multi-Layer Perceptron (MLP), for anomaly detection in microservices. The study covers the creation of a microservices infrastructure, the development of a fault injection module that simulates application-level and service-level anomalies, the creation of a system monitoring dataset, and the creation and validation of the MLP model to detect anomalies. The results indicate that the MLP model effectively detects anomalies in both domains with higher accuracy, precision, recovery, and F1 score on the service-level anomaly dataset. The potential for more effective distributed system monitoring and management automation is highlighted in this study by focusing on service-level metrics such as service response times. This study provides valuable information about the effectiveness of supervised machine learning models in detecting anomalies across distributed software systems.