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.

Abstract
Reducing vibration and noise in electrical machines for a given application is not a straightforward task, especially when the application imposes some restrictions. There are many techniques for reducing vibration based on design or control. Switched reluctance motors (SRMs) have a double-saliency structure, which results in a radial pulsation force. Consequently, they cause vibration and acoustic noise. This paper investigates the correlation between the radial force and the skew angle of the stator and/or rotor circuits. We computed the analysis from two-dimensional (2D) transient magnetic finite-element analysis (FEA) of three machine topologies, namely the 12/8 three-phase SRM, the 6/4 three-phase SRM and the 8/6 four-phase SRM. Compared to SRM, these topologies have the same basic dimensions (stator outer diameter, rotor outer diameter, and length) and operate in the same magnetic circuit saturation. The flux linkage and torque characteristics of the different motors are presented. The radial force distributed on the stator yoke under various skewing angles is studied extensively by FEA for the three machines. It is also demonstrated the effect of skewing angles in the reduction of radial force without any reduction in torque production. © 2023, Universidade do Porto - Faculdade de Engenharia. All rights reserved.