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 data-collection 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. © The Author(s), under exclusive license to Springer Nature Switzerland AG 2026.

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
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.

Abstract

Abstract
The ability to assess molecular binding kinetics in real time is critical for advancing our understanding of molecular interactions in biochemical and biotechnological systems. This work presents a novel optical tweezer (OT)-based method to monitor molecular affinity in real time, focusing on the high-affinity streptavidin-biotin system as a model. Transparent poly(methyl methacrylate) (PMMA) microparticles functionalized with streptavidin were trapped before, during, and after binding with biotinylated bovine serum albumin (biotin-BSA), enabling the analysis of forward-scattered signals to detect nanoscale changes in particle size. By applying the Power Spectral Density method, the friction coefficient of individual particles was calculated, allowing for real-time tracking of binding dynamics and the estimation of the association rate constant (kon approximate to 106M-1s-1). These results are consistent with literature values and demonstrate the potential of this OT-based approach for non-invasive, label-free detection of molecular interactions. Compared to existing techniques, such as atomic force microscopy and cantilever-based sensors, this method offers significant advantages, including real-time monitoring, adaptability to different bioaffinity systems, and compatibility with miniaturized setups. This work establishes a foundation for using OT-based tools to monitor high-affinity molecular interactions in real time. While demonstrated here using biotinylated BSA as a model ligand, future studies will explore the method's applicability to smaller ligands and more subtle surface modifications.