Showing 1–8 of 8 results for author: Howar, F

Language-Driven Engineering An Interdisciplinary Software Development Paradigm

Authors: Bernhard Steffen, Tiziana Margaria, Alexander Bainczyk, Steve Boßelmann, Daniel Busch, Marc Driessen, Markus Frohme, Falk Howar, Sven Jörges, Marvin Krause, Marco Krumrey, Anna-Lena Lamprecht, Michael Lybecait, Alnis Murtovi, Stefan Naujokat, Johannes Neubauer, Alexander Schieweck, Jonas Schürmann, Steven Smyth, Barbara Steffen, Fabian Storek, Tim Tegeler, Sebastian Teumert, Dominic Wirkner, Philip Zweihoff

Abstract: 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 application… ▽ More 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. △ Less

Submitted 16 February, 2024; originally announced February 2024.

Comments: 43 pages, 30 figures

Scalable Tree-based Register Automata Learning

Authors: Simon Dierl, Paul Fiterau-Brostean, Falk Howar, Bengt Jonsson, Konstantinos Sagonas, Fredrik Tåquist

Abstract: 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 bet… ▽ More 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^λ$, 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^λ$ 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. △ Less

Submitted 25 January, 2024; originally announced January 2024.

Comments: 26 pages, 8 figures, to appear in TACAS 2024

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

Authors: Till Schallau, Stefan Naujokat, Fiona Kullmann, Falk Howar

Abstract: 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 sc… ▽ More 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. △ Less

Submitted 11 July, 2023; originally announced July 2023.

Interpretable Anomaly Detection via Discrete Optimization

Authors: Simon Lutz, Florian Wittbold, Simon Dierl, Benedikt Böing, Falk Howar, Barbara König, Emmanuel Müller, Daniel Neider

Abstract: Anomaly detection is essential in many application domains, such as cyber security, law enforcement, medicine, and fraud protection. However, the decision-making of current deep learning approaches is notoriously hard to understand, which often limits their practical applicability. To overcome this limitation, we propose a framework for learning inherently interpretable anomaly detectors from sequ… ▽ More Anomaly detection is essential in many application domains, such as cyber security, law enforcement, medicine, and fraud protection. However, the decision-making of current deep learning approaches is notoriously hard to understand, which often limits their practical applicability. To overcome this limitation, we propose a framework for learning inherently interpretable anomaly detectors from sequential data. More specifically, we consider the task of learning a deterministic finite automaton (DFA) from a given multi-set of unlabeled sequences. We show that this problem is computationally hard and develop two 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 that our approach shows promising results in terms of accuracy and F1 score. △ Less

Submitted 24 March, 2023; originally announced March 2023.

ACM Class: F.4.3; I.2.6

Automatic Seizure Detection Using the Pulse Transit Time

Authors: Eric Fiege, Salima Houta, Pinar Bisgin, Rainer Surges, Falk Howar

Abstract: 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 an… ▽ More 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. △ Less

Submitted 13 July, 2021; originally announced July 2021.

Grey-Box Learning of Register Automata

Authors: Bharat Garhewal, Frits Vaandrager, Falk Howar, Timo Schrijvers, Toon Lenaerts, Rob Smits

Abstract: 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… ▽ More 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. △ Less

Submitted 21 September, 2020; originally announced September 2020.

Comments: To be published in iFM'2020 27 pages, 6 figures, 1 table

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

Authors: Adina Aniculaesei, Daniel Arnsberger, Falk Howar, Andreas Rausch

Abstract: 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 syst… ▽ More 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. △ Less

Submitted 15 December, 2016; originally announced December 2016.

Comments: In Proceedings V2CPS-16, arXiv:1612.04023

Journal ref: EPTCS 232, 2016, pp. 79-90

Verifying the Safety of a Flight-Critical System

Authors: Guillaume Brat, David Bushnell, Misty Davies, Dimitra Giannakopoulou, Falk Howar, Temesghen Kahsai

Abstract: 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 veri… ▽ More 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. △ Less

Submitted 9 February, 2015; originally announced February 2015.

Comments: 17 pages, 5 figures