Manuel Abreu, LuΓs Garrote, LuΓs Conde Bento,
Bradley Schmerl, Urbano J Nunes and
David Garlan. Formal Verification of Deep Neural Networks for Classification in Industrial Environments. In Proc. the 16th International Conference on Information Science and Technology, Coimbra, Portugal. October 1-6, 2026.
Abstract: Deep Learning methods, particularly Convolutional Neural Networks (CNN), have become widely adopted in indus- trial computer vision applications due to their strong image classification capabilities. In industrial environments, reliable object recognition is essential for automated systems such as warehouse automation and sorting processes, where incorrect classifications may lead to operational failures and reduced system reliability. Despite their performance, CNN-based models remain vulnerable to adversarial perturbations, raising concerns regarding their deployment in safety-critical applications. Industrial vision systems deployed in safety-critical environ- ments must operate reliably under adversarial perturbations and common perception degradations. This work presents a robustness analysis of image classification models for industrial environments using RGB and RGB-D data. An industrial object dataset containing seven classes was constructed through an ob- ject detection and extraction pipeline, resulting in object-centered image samples. Two CNN-based architectures were developed and evaluated: a baseline RGB model and a multimodal RGB-D model. Model robustness was analyzed through both formal verifica- tion and corruption-based robustness evaluation. Formal verifi- cation was performed using the alpha-beta-CROWN framework under different perturbation magnitudes, assessing whether the CNNs preserve their predictions under bounded perturbations. In addition, corruption-based experiments following the ImageNet- C protocol were conducted to evaluate model behavior under common image degradations.
π
Maria Casimiro,
Valentim RomΓ£o, Paolo Romano, Luis Rodrigues and
David Garlan. Ripple: A Long-Sighted Self-Adaptation Approach to Retrain Machine Learning-Enabled Systems. In Proc. 21st International Conference on Software Engineering for Adaptive and Self-Managing Systems (SEAMS), Rio de Janiero, Brazil. April 13-14, 2026.
https://doi.org/3788550.3794867.
Awarded Best Student Paper.
Abstract: Machine Learning (ML)-enabled systems are now ubiquitous. These systems leverage ML models that require frequent re-trainings, which can lead to unsustainable costs. To prevent superfluous retrains and optimize system performance in the long run, we introduce Ripple, a system that leverages probabilistic model checking techniques to automate the decision of when to retrain the ML models employed by an ML-enabled system. The main challenge tackled by Ripple is estimating how the predictive quality of an ML model varies over long-term horizons, both when it is and when it is not retrained. Ripple introduces Look-Ahead Adaptation Impact Predictors (LA-AIPs) that are used in combination with a probabilistic model checker to determine whether to retrain the ML model. This allows Ripple to optimize system performance in the long term, contributing to creating more sustainable ML-enabled systems. We demonstrate Rippleβs feasibility via a fraud detection system use case, showcasing its ability to plan for the long term and to account for retrain latency, improving over myopic adaptation approaches.
Abstract: Distributed Denial of Service (DDoS) attacks have grown in complexity, with attackers dynamically adapting their strategies to maximize disruption. Dynamic DDoS adversaries evolve their attacks by changing targets, modifying botnet infrastructure, or altering traffic patterns to evade detection and maintain attack effectiveness. This dynamic nature poses significant challenges for DDoS defense, particularly in developing scalable and robust adaptive systems capable of real-time response. This paper introduces a novel, robust, multilayered defense system called DosSink that integrates detection and mitigation through variational autoencoders (VAE) and actor-critic deep reinforcement learning (DRL). The VAE effectively reduces the feature space which may make the learning intractable and characterizes traffic to estimate the risk score for each flow. At the same time, the DRL agent uses these risk scores to optimize mitigation policies that include traffic limiting, flow redirection, or puzzle-based source verification actions. Feedback from puzzle inquiries refines VAE risk assessments, enhancing detection accuracy. Key innovations of this framework include (1) the VAE's adaptability as an anomaly detector that evolves with DRL actions, avoiding reliance on static rules or predefined thresholds and enhancing the robustness of the overall system adaptation; (2) the separation of traffic characterization (VAE) and decisionmaking (DRL), improving scalability by reducing the state space; and (3) real-time adaptability to evolving attackers' strategies through dynamic collaboration between the VAE and DRL. Our evaluation experiments show that this framework accurately identifies malicious traffic flows, with a true positive rate of over 98% and a false positive rate below 1 %. Moreover, it efficiently learns the optimal mitigation strategy in under 20, 000 episodes across most experimental settings.
Abstract: Temporal logic specifications play an important role in a wide range of software analysis tasks, such as model checking, automated synthesis, program comprehension, and runtime monitoring. Given a set of positive and negative examples, specified as traces, LTL learning is the problem of synthesizing a specification, in linear temporal logic (LTL), that evaluates to true over the positive traces and false over the negative ones. In this paper, we propose a new type of LTL learning problem called constrained LTL learning, where the user, in addition to positive and negative examples, is given an option to specify one or more constraints over the properties of the LTL formula to be learned. We demonstrate that the ability to specify these additional constraints significantly increases the range of applications for LTL learning, and also allows efficient generation of LTL formulas that satisfy certain desirable properties (such as minimality). We propose an approach for solving the constrained LTL learning problem through an encoding in first-order relational logic and reduction to an instance of the maximal satisfiability (MaxSAT) problem. An experimental evaluation demonstrates that ATLAS, an implementation of our proposed approach, is able to solve new types of learning problems while performing better than or competitively with the state-of-the-art tools in LTL learning.
Abstract: Cyber-physical systems (CPS) with reinforcement learning (RL)-based controllers are increasingly being deployed in complex phys- ical environments such as autonomous vehicles, the Internet-of-Things (IoT), and smart cities. An important property of a CPS is tolerance; i.e., its ability to function safely under possible disturbances and un- certainties in the actual operation. In this paper, we introduce a new, expressive notion of tolerance that describes how well a controller is ca- pable of satisfying a desired system requirement, specified using Signal Temporal Logic (STL), under possible deviations in the system. Based on this definition, we propose a novel analysis problem, called the tol- erance falsification problem, which involves finding small deviations that result in a violation of the given requirement. We present a novel, two- layer simulation-based analysis framework and a novel search heuristic for finding small tolerance violations. To evaluate our approach, we con- struct a set of benchmark problems where system parameters can be configured to represent different types of uncertainties and disturbances in the system. Our evaluation shows that our falsification approach and heuristic can effectively find small tolerance violations.
π
Abstract: This work focuses on the problem of hyper-parameter tuning (HPT) for robust (i.e., adversarially trained) models, shedding light on the new challenges and opportunities arising during the HPT process for robust models. To this end, we conduct an extensive experimental study based on three popular deep models and explore exhaustively nine (discretized) hyper-parameters (HPs), two fidelity dimensions, and two attack bounds, for a total of 19208 configurations (corresponding to 50 thousand GPU hours).
Through this study, we show that the complexity of the HPT problem is further exacerbated in adversarial settings due to the need to independently tune the HPs used during standard and adversarial training: succeeding in doing so (i.e., adopting different HP settings in both phases) can lead to a reduction of up to 80% and 43% of the error for clean and adversarial inputs, respectively. We also identify new opportunities to reduce the cost of HPT for robust models. Specifically, we propose to leverage cheap adversarial training methods to obtain inexpensive, yet highly correlated, estimations of the quality achievable using more robust/expensive state-of-the-art methods. We show that, by exploiting this novel idea in conjunction with a recent multi-fidelity optimizer (taKG), the efficiency of the HPT process can be enhanced by up to 2.1x.
Abstract: Machine Learning (ML) models are now commonly
used as components in systems. As any other component, ML
components can produce erroneous outputs that may penalize
system utility. In this context, self-adaptive systems emerge as
a natural approach to cope with ML mispredictions, through
the execution of adaptation tactics such as model retraining. To
synthesize an adaptation strategy, the self-adaptation manager
needs to reason about the cost-benefit tradeoffs of the applicable
tactics, which is a non-trivial task for tactics such as model
retraining, whose benefits are both context- and data-dependent.
To address this challenge, this paper proposes a probabilistic
modeling framework that supports automated reasoning about
the cost/benefit tradeoffs associated with improving ML components of ML-based systems. The key idea of the proposed approach is to decouple the problems of (i) estimating the expected
performance improvement after retrain and (ii) estimating the
impact of ML improved predictions on overall system utility.
We demonstrate the application of the proposed framework by
using it to self-adapt a state-of-the-art ML-based fraud-detection
system, which we evaluate using a publicly-available, real fraud
detection dataset. We show that by predicting system utility stemming from retraining a ML component, the probabilistic model
checker can generate adaptation strategies that are significantly
closer to the optimal, as compared against baselines such as
periodic retraining, or reactive retraining.
Abstract: Machine Learning (ML) is increasingly used in domains such
as cyber-physical systems and enterprise systems. These systems typically operate in non-static environments, prone to unpredictable changes that can adversely impact the accuracy of the ML models, which are usually in the critical path of the systems. Mispredictions of ML components
can thus affect other components in the system, and ultimately impact overall system utility in non-trivial ways. From this perspective, self-adaptation techniques appear as a natural solution to reason about how to react to environment changes via adaptation tactics that can
potentially improve the quality of ML models (e.g., model retrain), and ultimately maximize system utility. However, adapting ML components is non-trivial, since adaptation tactics have costs and it may not be clear in a given context whether the benefits of ML adaptation outweigh its
costs. In this paper, we present a formal probabilistic framework, based on model checking, that incorporates the essential governing factors for reasoning at an architectural level about adapting ML classifiers in a
system context. The proposed framework can be used in a self-adaptive system to create adaptation strategies that maximize rewards of a multidimensional utility space. Resorting to a running example from the enterprise
systems domain, we show how the proposed framework can be
employed to determine the gains achievable via ML adaptation and to find the boundary that renders adaptation worthwhile.
Maria Casimiro, Paolo Romano,
David Garlan,
Gabriel A. Moreno,
Eunsuk Kang and Mark Klein. Self-Adaptation for Machine Learning Based Systems. In Proceedings of the 1st International Workshop on Software Architecture and Machine Learning (SAML), Virtual, (Originally VΓ€xjΓΆ, Sweden), Springer. LNCS. September 14, 2021.
Abstract: TodayΓ’β¬β’s world is witnessing a shift from human-written software to machine-learned software, with the rise of systems
that rely on machine learning. These systems typically operate in non-static environments, which are prone to unexpected
changes, as is the case of self-driving cars and enterprise systems. In this context, machine-learned software can misbehave.
Thus, it is paramount that these systems are capable of detecting problems with their machined-learned components and
adapt themselves to maintain desired qualities. For instance, a fraud detection system that cannot adapt its machine-learned
model to efficiently cope with emerging fraud patterns or changes in the volume of transactions is subject to losses of millions
of dollars. In this paper, we take a first step towards the development of a framework aimed to self-adapt systems that rely
on machine-learned components. We describe: (i) a set of causes of machine-learned component misbehavior and a set of
adaptation tactics inspired by the literature on machine learning, motivating them with the aid of a running example; (ii) the
required changes to the MAPE-K loop, a popular control loop for self-adaptive systems; and (iii) the challenges associated
with developing this framework. We conclude the paper with a set of research questions to guide future work.
Abstract: In software design, guaranteeing the correctness of run-time system behavior while achieving an acceptable balance among multiple quality attributes remains a challenging problem.
Moreover, providing guarantees about the satisfaction of those requirements when systems are subject to uncertain environments is even more challenging.
While recent developments in architectural analysis techniques can assist architects in exploring the satisfaction of quantitative guarantees across the design space, existing approaches are still limited because they do not explicitly link design decisions to satisfaction of quality requirements.
Furthermore, the amount of information they yield can be overwhelming to a human designer, making it difficult to distinguish the forest through the trees.
In this paper, we present an approach to analyzing architectural design spaces that addresses these limitations and provides a basis to enable the explainability of design tradeoffs.
Our approach combines dimensionality reduction techniques employed in machine learning pipelines with quantitative verification to enable architects to understand how design decisions contribute to the satisfaction of strict quantitative guarantees under uncertainty across the design space.
Our results show feasibility of the approach in two case studies and evidence that dimensionality reduction is a viable approach to facilitate comprehension of tradeoffs in poorly-understood design spaces.
Marin Litoiu, Necmiye Ozay, Colin Paterson, Kenji Tei, Alberto Leva, Masako Kishida,
Bradley Schmerl and Danny Weyns. Towards Better Adaptive Systems by Combining MAPE, Control Theory, and Machine Learning. In Proceedings of the 16th Symposium on Software Engineering for Adaptive and Self-Managing Systems, Virtual. May 17-24, 2021.
https://doi.org/10.1109/seams51251.2021.00036.
Abstract: Two established techniques to engineer adaptive systems are architecture-based adaptation that uses a Monitor-Analysis-Planning-Executing (MAPE) loop that reasons over architectural models (aka Knowledge) to make adaptation decisions, and control-based adaptation that relies on principles of control theory (CT) to realize adaptation.
Recently, we also observe a rapid growing interest in applying machine learning (ML) to support different adaptation mechanisms.
While MAPE and CT have particular characteristics and strengths to be applied independently, in this paper we are concerned with the question of how these techniques are related with one another and whether combining them and supporting them with ML can produce better adaptive systems.
We motivate the combined use of different adaptation techniques using scenarios from two different domains and illustrate the analysis involved in combining different adaptation techniques. The paper concludes with suggestions for further research in this interesting area.
Abstract: Self-adaptive software systems rely on planning to
make adaptation decisions autonomously. Planning is required
to produce high-quality adaptation plans in a timely manner;
however, quality and timeliness of planning are conflicting in
nature. This conflict can be reconciled with hybrid planning,
which can combine reactive planning (to quickly provide an
emergency response) with deliberative planning that take time
but determine a higher-quality plan. While often effective, reactive
planning sometimes risks making the situation worse. Hence,
a challenge in hybrid planning is to decide whether to invoke
reactive planning until the deliberative planning is ready with a
high-quality plan. To make this decision, this paper proposes a
novel learning-based approach. We demonstrate that this learning-based
approach outperforms existing techniques that are based
on specifying fixed conditions to invoke reactive planning in two
domains: enterprise cloud systems and unmanned aerial vehicles.
Abstract: Modern data analytic and machine learning jobs
find in the cloud a natural deployment platform to satisfy their
notoriously large resource requirements. Yet, to achieve cost
efficiency, it is crucial to identify a deployment configuration that
satisfies user-defined QoS constraints (e.g., on execution time),
while avoiding unnecessary over-provisioning.
This paper introduces Lynceus, a new approach for the
optimization of cloud-based data analytic jobs that improves over
state-of-the-art approaches by enabling significant cost savings
both in terms of the final recommended configuration and of the
optimization process used to recommend configurations.
Unlike existing solutions, Lynceus optimizes in a joint fashion
both the cloud-related (i.e., which and how many machines to
provision) and the application-level (e.g. the hyper-parameters
of a machine learning algorithm) parameters. This allows for a
reduction of the cost of recommended configurations by up to
3.7X at the 90-th percentile with respect to existing approaches,
which treat the optimization of cloud-related and application level
parameters as two independent problems.
Further, Lynceus reduces the cost of the optimization process
(i.e., the cloud cost incurred for testing configurations) by
up to 11X. Such an improvement is achieved thanks to two
mechanisms: i) a timeout approach which allows to abort the
exploration of configurations that are deemed suboptimal, while
still extracting useful information to guide future explorations
and to improve its predictive model Γ’β¬β differently from recent
works, which either incur the full cost for testing suboptimal
configurations or are unable to extract any knowledge from
aborted runs; ii) a long-sighted and budget-aware technique
that determines which configurations to test by predicting the
long-term impact of each exploration Γ’β¬β unlike state-of-the-art
approaches for the optimization of cloud jobs, which adopt greedy
optimization methods.
Abstract: This work introduces TrimTuner, the first system for optimizing machine learning jobs in the cloud to exploit sub-sampling techniques to reduce the cost of the optimization process, while keeping into account user-specified constraints. TrimTuner jointly optimizes the cloud and application-specific parameters and, unlike state of the art works for cloud optimization, eschews the need to train the model with the full training set every time a new configuration is sampled. Indeed, by leveraging sub-sampling techniques and data-sets that are up to 60x smaller than the original one, we show that TrimTuner can reduce the cost of the optimization process by up to 50x. Further, TrimTuner speeds-up the recommendation process by 65Γβwith respect to state of the art techniques for hyper-parameter optimization that use sub-sampling techniques. The reasons for this improvement are twofold: i) a novel domain specific heuristic that reduces the number of configurations for which the acquisition function has to be evaluated; ii) the adoption of an ensemble of decision trees that enables boosting the speed of the recommendation process by one additional order of magnitude.