Abstract
Alloy is a lightweight formal method that is well suited to teaching logic because it combines expressive logics with automatic analysis and visual feedback. In this paper, we report our experience using specification challenges on the Alloy4Fun platform in our formal methods courses. We briefly describe the types of challenges we have used over the years and discuss how different hints can help students make progress in solving them. Our main conclusion is that specification challenges are highly engaging and useful for students, but they should be balanced with broader modeling and validation activities to support long-term learning outcomes. They are also useful for research, because Alloy4Fun's datacollection infrastructure enables the release of open datasets that can be mined for insights into Alloy usage and for the evaluation of new tools and techniques.

Abstract

Abstract
Early fault detection remains a critical challenge in predictive maintenance (PdM), particularly within critical infrastructure, where undetected failures or delayed interventions can compromise safety and disrupt operations. Traditional anomaly detection methods are typically reactive, relying on real-time sensor data to identify deviations as they occur. This reactive nature often provides insufficient lead time for effective maintenance planning. To address this limitation, we propose a novel two-stage early detection framework that integrates time series forecasting with anomaly detection to anticipate equipment failures several hours in advance. In the first stage, future sensor signal values are predicted using forecasting models; in the second, conventional anomaly detection algorithms are applied directly to the forecasted data. By shifting from real-time to anticipatory detection, the framework aims to deliver actionable early warnings, enabling timely and preventive maintenance. We validate this approach through a case study focused on metro train systems, an environment where early fault detection is crucial for minimizing service disruptions, optimizing maintenance schedules, and ensuring passenger safety. The framework is evaluated across three forecast horizons (1, 3, and 6 hours ahead) using twelve state-of-the-art anomaly detection algorithms from diverse methodological families. Detection performance is assessed using five performance metrics. Results show that anomaly detection remains highly effective at short to medium horizons, with performance at 1-hour and 3-hour forecasts comparable to that of real-time data. Ensemble and deep learning models exhibit strong robustness to forecast uncertainty, maintaining consistent results with real-time data even at 6-hour forecasts. In contrast, distance- and density-based models suffer substantial degradation at longer horizons (6-hours), reflecting their sensitivity to distributional shifts in predicted signals. Overall, the proposed framework offers a practical and extensible solution for enhancing traditional PdM systems with proactive capabilities. By enabling early anomaly detection on forecasted data, it supports improved decision-making, operational resilience, and maintenance planning in industrial environments.

Abstract

Abstract
Generative artificial intelligence (GenAI) promises substantial productivity gains for organisations, yet unresolved questions about data management and privacy continue to shape managers' and employees' confidence. This study examines workplace adoption of GenAI and shows how trust, conditioned by perceptions of data-management integrity, information transparency, and privacy risk, influences acceptance. This mixed-method study tests, using a survey-based structural equation model plus interviews focused on managerial practices among daily GenAI practitioners, two core insights: (i) trust is the strongest predictor of intention to use GenAI, and (ii) trust depends chiefly on manager's and employees' belief that organisational data are handled reliably and objectively through management routines. Perceptions of transparency or privacy risk exert no direct influence on either trust or usage. Building on these results, the study delineates four managerial domains: data-management process, information transparency, privacy risk, and trust, alongside twenty future research questions designed to understand how GenAI is linked to managerial practices. For practice, the findings recommend monitoring, calibrated disclosure, and adaptive privacy protocols as concrete managerial levers to strengthen GenAI acceptance. The evidence highlights trustworthy data governance, not abstract explainability, as the foundation of sustainable GenAI adoption. The study also provides a roadmap of actionable management practices to guide its implementation in modern workplaces.

Abstract
Context: Software testing is an often used method to ensure software quality, with developers spending a significant amount of time on it. However, software testing education is underrepresented in curricula, particularly with regard to Conceptual Modelling (CM), where model-level validation is important. As a consequence, graduate students are insufficiently prepared for industry-level testing. Objective: We want to understand students' behavioural patterns during model testing and their relationship to testing effectiveness.Method: We use process mining to analyze 554 interaction logs from students using a conceptual model simulation tool.Results: We identify three strategies: the coverage chaser (using feedback iteratively), the problem solver (balancing feedback with requirements focus), and the disconnected tester (avoiding feedback-driven iteration). High-coverage students integrated feedback into test loops; low-coverage students did not. Notably, high and average-coverage students achieved similar grades, suggesting a plateau where systematic testing enables sufficient educational performance without requiring maximum coverage.Conclusions: Our findings highlight the importance of teaching students to systematically use coverage feedback to guide test design in CM contexts.