arXiv subjects

Falk Howar

Publications and source records attributed to Falk Howar.

12 recordsLinked to original sources

arXiv2025

ARRC: Explainable, Workflow-Integrated Recommender for Sustainable Resource Optimization Across the Edge-Cloud Continuum

Achieving sustainable, explainable, and maintainable automation for resource optimization is a core challenge across the edge-cloud continuum. Persistent overprovisioning and operational complexity often stem from heterogeneous platforms and layered abstractions, while systems lacking explainability and maintainability become fragile, impede safe recovery, and accumulate technical debt. Existing solutions are frequently reactive, limited to single abstraction layers, or require intrusive platform changes, leaving efficiency and maintainability gains unrealized. This paper addresses safe, transparent, and low-effort resource optimization in dynamic, multi-tenant edge-cloud systems, without disrupting operator workflows or increasing technical debt. We introduce ARRC, a recommender system rooted in software engineering design principles, which delivers explainable, cross-layer resource recommendations directly into operator workflows (such as tickets and GitOps pull requests). ARRC encapsulates optimization logic in specialized, auditable agents coordinated via a shared interface, supporting maintainability and extensibility through transparency and the ability to inspect both recommendations and their rationale. Empirical evaluation in a multi-region industrial deployment shows that ARRC reduces operator workload by over 50%, improves compute utilization by up to 7.7x, and maintains error rates below 5%, with most benefits achieved through incremental, operator-approved changes. This demonstrates that explainable, recommendation-based architectures can achieve sustainable efficiency and maintainability improvements at production scale. ARRC provides an empirically evaluated framework for integrating explainable, workflow-driven automation into resource management, intended to advance best practices for robust, maintainable, and transparent edge-cloud continuum platforms.

cs.DC↗

arXiv2025

GMB-ECC: Guided Measuring and Benchmarking of the Edge Cloud Continuum

In the evolving landscape of cloud computing, optimizing energy efficiency across the edge-cloud continuum is crucial for sustainability and cost-effectiveness. We introduce GMB-ECC, a framework for measuring and benchmarking energy consumption across the software and hardware layers of the edge-cloud continuum. GMB-ECC enables energy assessments in diverse environments and introduces a precision parameter to adjust measurement complexity, accommodating system heterogeneity. We demonstrate GMB-ECC's applicability in an autonomous intra-logistic use case, highlighting its adaptability and capability in optimizing energy efficiency without compromising performance. Thus, this framework not only assists in accurate energy assessments but also guides strategic optimizations, cultivating sustainable and cost-effective operations.

cs.DC↗

arXiv2025

Innamark: A Whitespace Replacement Information-Hiding Method

Large language models (LLMs) have gained significant popularity in recent years. Differentiating between a text written by a human and one generated by an LLM has become almost impossible. Information-hiding techniques such as digital watermarking or steganography can help by embedding information inside text in a form that is unlikely to be noticed. However, existing techniques, such as linguistic-based or format-based methods, change the semantics or cannot be applied to pure, unformatted text. In this paper, we introduce a novel method for information hiding called Innamark, which can conceal any byte-encoded sequence within a sufficiently long cover text. This method is implemented as a multi-platform library using the Kotlin programming language, which is accompanied by a command-line tool and a web interface. By substituting conventional whitespace characters with visually similar Unicode whitespace characters, our proposed scheme preserves the semantics of the cover text without changing the number of characters. Furthermore, we propose a specified structure for secret messages that enables configurable compression, encryption, hashing, and error correction. An experimental benchmark comparison on a dataset of 1 000 000 Wikipedia articles compares ten algorithms. The results demonstrate the robustness of our proposed Innamark method in various applications and the imperceptibility of its watermarks to humans. We discuss the limits to the embedding capacity and robustness of the algorithm and how these could be addressed in future work.

cs.CR↗

arXiv2024

Bounds for Quantum Circuits using Logic-Based Analysis

We explore ideas for scaling verification methods for quantum circuits using SMT (Satisfiability Modulo Theories) solvers. We propose two primary strategies: (1) decomposing proof obligations via compositional verification and (2) leveraging linear over-approximation techniques for gate effects. We present two examples and demonstrate the application of these ideas to proof Hamming weight preservation.

cs.LO↗

arXiv2024

Language-Driven Engineering An Interdisciplinary Software Development Paradigm

We illustrate how purpose-specific, graphical modeling enables application experts with different levels of expertise to collaboratively design and then produce complex applications using their individual, purpose-specific modeling language. Our illustration includes seven graphical Integrated Modeling Environments (IMEs) that support full code generation, as well as four browser-based applications that were modeled and then fully automatically generated and produced using DIME, our most complex graphical IME. While the seven IMEs were chosen to illustrate the types of languages we support with our Language-Driven Engineering (LDE) approach, the four DIME products were chosen to give an impression of the power of our LDE-generated IMEs. In fact, Equinocs, Springer Nature's future editorial system for proceedings, is also being fully automatically generated and then deployed at their Dordrecht site using a deployment pipeline generated with Rig, one of the IMEs presented. Our technology is open source and the products presented are currently in use.

cs.SE↗

arXiv2024

Scalable Tree-based Register Automata Learning

Existing active automata learning (AAL) algorithms have demonstrated their potential in capturing the behavior of complex systems (e.g., in analyzing network protocol implementations). The most widely used AAL algorithms generate finite state machine models, such as Mealy machines. For many analysis tasks, however, it is crucial to generate richer classes of models that also show how relations between data parameters affect system behavior. Such models have shown potential to uncover critical bugs, but their learning algorithms do not scale beyond small and well curated experiments. In this paper, we present $SL^\lambda$, an effective and scalable register automata (RA) learning algorithm that significantly reduces the number of tests required for inferring models. It achieves this by combining a tree-based cost-efficient data structure with mechanisms for computing short and restricted tests. We have implemented $SL^\lambda$ as a new algorithm in RALib. We evaluate its performance by comparing it against $SL^*$, the current state-of-the-art RA learning algorithm, in a series of experiments, and show superior performance and substantial asymptotic improvements in bigger systems.

cs.FL↗

arXiv2023

Tree-Based Scenario Classification: A Formal Framework for Coverage Analysis on Test Drives of Autonomous Vehicles

Scenario-based testing is envisioned as a key approach for the safety assurance of autonomous vehicles. In scenario-based testing, relevant (driving) scenarios are the basis of tests. Many recent works focus on specification, variation, generation and execution of individual scenarios. In this work, we address the open challenges of classifying sets of scenarios and measuring coverage of theses scenarios in recorded test drives. Technically, we define logic-based classifiers that compute features of scenarios on complex data streams and combine these classifiers into feature trees that describe sets of scenarios. We demonstrate the expressiveness and effectiveness of our approach by defining a scenario classifier for urban driving and evaluating it on data recorded from simulations.

cs.SE↗

arXiv2023

Unsupervised Automata Learning via Discrete Optimization

Automata learning is a successful tool for many application domains such as robotics and automatic verification. Typically, automata learning techniques operate in a supervised learning setting (active or passive) where they learn a finite state machine in contexts where additional information, such as labeled system executions, is available. However, other settings, such as learning from unlabeled data - an important aspect in machine learning - remain unexplored. To overcome this limitation, we propose a framework for learning a deterministic finite automaton (DFA) from a given multi-set of unlabeled words. We show that this problem is computationally hard and develop three learning algorithms based on constraint optimization. Moreover, we introduce novel regularization schemes for our optimization problems that improve the overall interpretability of our DFAs. Using a prototype implementation, we demonstrate practical feasibility in the context of unsupervised anomaly detection.

cs.LG↗

arXiv2021

Automatic Seizure Detection Using the Pulse Transit Time

Documentation of epileptic seizures plays an essential role in planning medical therapy. Solutions for automated epileptic seizure detection can help improve the current problem of incomplete and erroneous manual documentation of epileptic seizures. In recent years, a number of wearable sensors have been tested for this purpose. However, detecting seizures with subtle symptoms remains difficult and current solutions tend to have a high false alarm rate. Seizures can also affect the patient's arterial blood pressure, which has not yet been studied for detection with sensors. The pulse transit time (PTT) provides a noninvasive estimate of arterial blood pressure. It can be obtained by using to two sensors, which are measuring the time differences between arrivals of the pulse waves. Due to separated time chips a clock drift emerges, which is strongly influencing the PTT. In this work, we present an algorithm which responds to alterations in the PTT, considering the clock drift and enabling the noninvasive monitoring of blood pressure alterations using separated sensors. Furthermore we investigated whether seizures can be detected using the PTT. Our results indicate that using the algorithm, it is possible to detect seizures with a Random Forest. Using the PTT along with other signals in a multimodal approach, the detection of seizures with subtle symptoms could thereby be improved.

cs.CV↗

arXiv2020

Grey-Box Learning of Register Automata

Model learning (a.k.a. active automata learning) is a highly effective technique for obtaining black-box finite state models of software components. Thus far, generalisation to infinite state systems with inputs/outputs that carry data parameters has been challenging. Existing model learning tools for infinite state systems face scalability problems and can only be applied to restricted classes of systems (register automata with equality/inequality). In this article, we show how we can boost the performance of model learning techniques by extracting the constraints on input and output parameters from a run, and making this grey-box information available to the learner. More specifically, we provide new implementations of the tree oracle and equivalence oracle from RALib, which use the derived constraints. We extract the constraints from runs of Python programs using an existing tainting library for Python, and compare our grey-box version of RALib with the existing black-box version on several benchmarks, including some data structures from Python's standard library. Our proof-of-principle implementation results in almost two orders of magnitude improvement in terms of numbers of inputs sent to the software system. Our approach, which can be generalised to richer model classes, also enables RALib to learn models that are out of reach of black-box techniques, such as combination locks.

cs.FL↗

arXiv2016

Towards the Verification of Safety-critical Autonomous Systems in Dynamic Environments

There is an increasing necessity to deploy autonomous systems in highly heterogeneous, dynamic environments, e.g. service robots in hospitals or autonomous cars on highways. Due to the uncertainty in these environments, the verification results obtained with respect to the system and environment models at design-time might not be transferable to the system behavior at run time. For autonomous systems operating in dynamic environments, safety of motion and collision avoidance are critical requirements. With regard to these requirements, Macek et al. [6] define the passive safety property, which requires that no collision can occur while the autonomous system is moving. To verify this property, we adopt a two phase process which combines static verification methods, used at design time, with dynamic ones, used at run time. In the design phase, we exploit UPPAAL to formalize the autonomous system and its environment as timed automata and the safety property as TCTL formula and to verify the correctness of these models with respect to this property. For the runtime phase, we build a monitor to check whether the assumptions made at design time are also correct at run time. If the current system observations of the environment do not correspond to the initial system assumptions, the monitor sends feedback to the system and the system enters a passive safe state.

cs.SE↗

arXiv2015

Verifying the Safety of a Flight-Critical System

This paper describes our work on demonstrating verification technologies on a flight-critical system of realistic functionality, size, and complexity. Our work targeted a commercial aircraft control system named Transport Class Model (TCM), and involved several stages: formalizing and disambiguating requirements in collaboration with do- main experts; processing models for their use by formal verification tools; applying compositional techniques at the architectural and component level to scale verification. Performed in the context of a major NASA milestone, this study of formal verification in practice is one of the most challenging that our group has performed, and it took several person months to complete it. This paper describes the methodology that we followed and the lessons that we learned.

cs.SE↗