Abstract
We focus on the integration of Formal Methods as mandatory theme in any Computer Science University curriculum. In particular, when considering the ACM Curriculum for Computer Science, the inclusion of Formal Methods as a mandatory Knowledge Area needs arguing for why and how does every computer science graduate benefit from such knowledge. We do not agree with the sentence While there is a belief that formal methods are important and they are growing in importance, we cannot state that every computer science graduate will need to use formal methods in their career. We argue that formal methods are and have to be an integral part of every computer science curriculum. Just as not all graduates will need to know how to work with databases either, it is still important for students to have a basic understanding of how data is stored and managed efficiently. The same way, students have to understand why and how formal methods work, what their formal background is, and how they are justified. No engineer should be ignorant of the foundations of their subject and the formal methods based on these. In this article, we aim at highlighting why every computer scientist needs to be familiar with formal methods. We argue that education in formal methods plays a key role by shaping students' programming mindset, fostering an appreciation for underlying principles, and encouraging the practice of thoughtful program

Abstract

This paper presents an integrated analytical approach to assess the reliability of power electronic converters in Permanent Magnet Synchronous Generator (PMSG)-based wind farms under variable wind conditions. The study focuses on analyzing the impact of wake effect turbulences and thermal management on power converter reliability, driven by the thermal stress induced by fluctuating wind speeds on power converters. Through extensive simulations using FLORIS and MATLAB, the thermal behavior of converters in wind farms affected by wake interactions was examined to identify potential reliability issues. The methodology involved modeling an 80-turbine wind farm in FLORIS to simulate wake effects, processing high-resolution wind speed data in MATLAB to refine wind speed profiles, and using Simulink to simulate the thermal profiles of power electronics. The results of FLORIS simulations highlighted the variations in turbulence intensity (TI) and power output, while the MATLAB and Simulink models quantified critical thermal stresses in power converters, correlating the locations of the turbine rows with temperature fluctuations and potential failures. Machine learning models, including Gradient Boosting and Random Forest Regressor, were utilized to refine and predict the multi-objective reliability function. The findings underscore the importance of understanding and managing thermal dynamics to improve the reliability and operational resilience of the power converter, supporting sustainable wind farm operations in dynamically changing wind conditions.

Abstract
Accurate traffic state prediction is fundamental to Intelligent Transportation Systems, playing a critical role in optimising traffic management, improving mobility, and enhancing the efficiency of transportation networks. Traditional methods often rely on feature engineering, statistical time-series approaches, and non-parametric techniques to model the inherent complexities of traffic states, incorporating external factors such as weather conditions and accidents to refine predictions. However, the effectiveness of long-term traffic state prediction hinges on capturing spatial-temporal dependencies over extended periods. Current models face challenges in dealing with (i) high-dimensional traffic features, (ii) error accumulation for multi-step prediction, and (iii) robustness to external factors effectively. To address these challenges, this study proposes a novel model with a Dynamic Feature Embedding layer designed to transform complex data sequences into meaningful representations and a Deep Linear Projection network that refines these representations through non-linear transformations and gating mechanisms. These two features make the model more scalable when dealing with high-dimensional traffic features. The model also includes a Spatial-Temporal Positional Encoding layer to capture spatial-temporal relationships, masked multi-head attention-based encoder blocks, and a Residual Temporal Convolutional Network to process features and extract short-and long-term temporal patterns. Finally, a Time-Distributed Fully Connected Layer produces accurate traffic state predictions up to 24 timesteps into the future. The proposed architecture uses a direct strategy for multi-step modelling to help predict timesteps non-autoregressively and thus circumvents the error accumulation problem. The model was evaluated against state-of-the-art baselines using two benchmark datasets. Experimental results demonstrated the model's superiority, achieving up to 21.17% and 29.30% average improvements in Root Mean Squared Error and 3.56% and 32.80% improvements in Mean Absolute Error compared to the baselines, respectively. The Friedman Chi-Square statistical test further confirmed the significant performance difference between the proposed model and its counterparts. The adversarial perturbations and random sensor dropout tests demonstrated its good robustness. On top of that, it demonstrated good generalizability through extensive experiments. The model effectively mitigates error accumulation in multi-step predictions while maintaining computational efficiency, making it a promising solution for enhancing Intelligent Transportation Systems.

Abstract
This work studies the influence of an Erbium-Doped Fiber Amplifier (EDFA) on the phase variation of light in an optical fiber. To this end, the state of polarization (SOP) was measured as a function of optical power by adjusting the EDFA amplification, for two different laser output powers (2 dBm and 5 dBm). Results show that phase variation correlates with changes in optical power in both cases.

Abstract
This paper examines the role of digital twins (DTs) in promoting sustainability within seaport operations and logistics. DTs have emerged as promising tools for enhancing seaport performance. Despite the recognized potential of DTs in seaports, there is a paucity of research on their practical implementation and impact on seaport sustainability. Through a systematic literature review, this study seeks to elucidate how DTs contribute to the sustainability of seaports and to identify future research and practical applications. We reviewed and categorized 68 conceptual and practical digital applications into ten core areas that effectively support economic, social, and environmental objectives in seaports. Furthermore, this paper proposes five preliminary potential applications for DTs where practical implementations are currently lacking. The primary findings indicate that DTs can enhance seaport sustainability by facilitating real-time monitoring and decision-making, improving safety and security, optimizing resource utilization, enhancing collaboration and communication, and supporting the development of the seaport ecosystem. Additionally, this study addresses the challenges associated with DT implementation, including high costs, conflicting stakeholder priorities, data quality and availability, and model validation. The paper concludes with a discussion of the implications for seaport managers and policymakers.

Abstract

Power quality (PQ) issues, including weak grids, voltage transients, harmonics, notches, current imbalance, and voltage sags, are critical challenges in the textile industry. Even a brief power interruption can halt industrial processes, leading to substantial financial losses. This paper proposes a Model Predictive Control (MPC)-based Unified Power Quality Conditioner (UPQC) as a robust solution to mitigate these PQ disturbances in textile industry-integrated distribution grids. The proposed UPQC is designed to enhance voltage stability, suppress harmonics, regulate reactive power, and correct current imbalance, ensuring uninterrupted industrial operation. A key contribution of this work is the realistic modeling of a textile industry’s electrical network, replicating actual industry ratings to evaluate system performance. The proposed MPC-based UPQC is assessed through five case studies, addressing weak vs. strong grids, voltage transients, current imbalance, and voltage sags—the most significant PQ challenges in textile applications. Simulation results demonstrate that the UPQC significantly improves voltage profiles, reduces harmonic distortion, and effectively compensates for current imbalance. Compared to conventional Proportional-Integral (PI) controllers, the MPC-based UPQC exhibits superior performance in dynamic PQ disturbance mitigation and grid stabilization. These findings underscore the proposed system’s suitability for large-scale industrial deployment, offering a cost-effective and robust solution to enhance operational efficiency and grid reliability in the textile sector.