Dear all,
on Wednesday, May 12, at 10:30 am, Mirco Giacobbe from the University of Oxford will give a talk on his recent work of applying neural networks to perform termination analysis.
Wednesday, 12.05.2021, 10:30 am
https://rwth.zoom.us/j/99669198425?pwd=NTNzTGNnYjNrQUc0ZDFTTVdiWjY4UT09
Meeting-ID: 996 6919 8425, Passcode: 878733
Everybody is welcome!
Best regards
Helen Bolke-Hermanns
-----------------------------------------------------------------------------------------
Mirco Giacobbe (University of Oxford, UK): Neural Termination Analysis
Termination analysis answers the question of whether a program always responds or, dually, never gets stuck in an infinite loop. This is unsolvable in general, yet tools that work in practice have been developed in industry and academia. The major existing methods construct termination proofs via symbolic reasoning from the source code. I will talk about a novel method for learning termination proofs from execution traces. We let neural networks fit termination witnesses over execution traces and then use satisfiability modulo theories for checking whether they generalise to all possible executions. Thanks to the ability of neural networks to generalise well, neural termination analysis succeeds over a wide variety of programs. Moreover, it is extremely simple to implement. I will talk about how we apply neural termination analysis to the termination analysis of Java programs that use data structures, to the almost-sure termination analysis of probabilistic programs, and to the stability analysis of cyber-physical systems.
More information: https://www.unravel.rwth-aachen.de/go/id/nyoee
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Mittwoch, 5. Mai 2021, 11.00 Uhr
Ort: Videokonferenz (Zoom-Meeting, Information siehe unten)
Referent: Martin Schweigler, M.Sc. RWTH
Informatik 11 - Embedded Software
Thema: Ground Surface Pattern Recognition for Enhanced Navigation
Abstract:
With the continuous increase in sales of electrical assisted bicycles over the last decade, the
number of bicycle accidents across Europe has simultaneously grown significantly. At the
same time the technology lacks on active safety systems, even though the electrification
of the so-called Pedelecs would allow their development. This dissertation can be seen as
the first step in the process of developing position and situation dependent active safety
systems by improving the position determination accuracy of bicycle navigation systems.
In the core of this work a position estimation system is developed, which uses road
sections with significant surface conditions to improve the positioning accuracy of a
conventional GNSS/INS. Based on the vertical accelerations acting on the moving Pedelec,
the system recognizes individual spots in the road surface, e.g. manholes or potholes. To
be more precise, the individual acceleration profiles that occur when passing different
spots, are recorded with a smartphone and statistically modeled offline with the help of
continuous hidden Markov models during the training phase. In online mode, the trained
models are then used to recognize the spots by the acceleration profiles of the revisited
road sections. The absolute positions of the Pedelec, relative to the global coordinates
of the recognized spots, are subsequently determined by an inertial calculation of the
distances traveled in the time between their detection and classification. The system thus
uses statistical models to estimate the absolute position of the Pedelec and is consequently
called Statistical Absolute Position Estimator, or SAPE.
In the second part of this work, SAPE is used to develop a navigation system, which
shows the potential of the ground surface pattern recognition. For this purpose the SAPE
and GNSS position determinations are fused with an inertial navigation system using an
extended Kalman filter. Since the inertial sensors provided by the chosen smartphone
are not accurate enough to realize a stand-alone INS, an odometry is developed and
implemented to support the navigation solution. The resulting GNSS, SAPE and
odometry supported INS is finally evaluated using an RTK GNSS and its accuracy is
compared to that of a conventional odometry supported GNSS/INS created with the
same low-cost hardware.
Es laden ein: die Dozentinnen und Dozenten der Informatik
********************************
Thema: Promotionsvortrag Martin Schweigler
Uhrzeit: 05. Mai 2021 11:00 AM Amsterdam, Berlin, Stockholm, Wien
Zoom-Meeting beitreten
https://rwth.zoom.us/j/96325334175?pwd=R2o3TWNKYk9kS0hWN3k3UHVhblNYZz09
Meeting-ID: 963 2533 4175
Kenncode: 988764
**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Dienstag, 15. Dezember 2020, 10:00 Uhr
Zoom:
https://rwth.zoom.us/j/99233095930?pwd=dHhTV253V1ZYUzRtSkk1L3A1REZVUT09
Meeting-ID: 992 3309 5930
Kenncode: 626162
Referent: Philipp Weidel, Dipl. Inform.
Thema: Learning and decision making in closed loop simulations of
plastic spiking neural networks
Abstract:
To understand how animals and humans learn, form memories and make
decisions is a highly relevant goal both for neuroscience and for fields
that take some inspiration from neuroscience, such as machine learning
and artificial intelligence. Many models of learning and decision making
were developed in the fields of machine learning, artificial
intelligence, and computational neuroscience. Although these models aim
to describe similar mechanisms, they do not all pursue the same goal.
These models can be differentiated between models aiming to reach
optimal performance on a specific task (or set of tasks) and models
trying to explain how animals and humans learn. Some models of the first
class use biologically inspired methods (such as deep learning) but are
usually not biologically realistic and are therefore not well suited to
explain the function of the brain. Models in the second class focus on
being biologically plausible to explain how the brain works, but often
demonstrate their capability on too simplistic tasks and yield low
performance on well-known tasks from machine learning. This work aims to
close the gap between these two types of models.
In the first part of this talk, tools are described that allow the
combination of biologically plausible neural network models together
with powerful toolkits known from machine learning and robotics. To this
end, MUSIC, the middleware for spiking neural network simulators such as
NEST and NEURON is interfaced with ROS, a middleware for robotic
hardware and simulators such as Gazebo. This toolchain is extended with
interfaces to reinforcement learning toolkits such as the OpenAI Gym.
The second part addresses the question of how the brain can represent
its environment in the neural substrate of the cortex and how a
realistic model of reinforcement learning can make use of these
representations. To this end, a spiking neural network model of
unsupervised learning is presented which is able to learn its input
projections such that it can detect and represent repeating patterns. By
using an actor-critic reinforcement learning architecture driven by a
realistic dopamine modulated plasticity rule the model can make use of
the representations and learn a range tasks.
Es laden ein: die Dozentinnen und Dozenten der Informatik
--
Prof. Dr. Abigail Morrison
IAS-6 / INM-6 / SimLab Neuroscience
Jülich Research Center
&
Computer Science 3 - Software Engineering
RWTH Aachen
http://www.fz-juelich.de/inm/inm-6http://www.fz-juelich.de/ias/jsc/slnshttp://www.se-rwth.de
Office: +49 2461 61-9805
Fax # : +49 2461 61-9460
------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------
Forschungszentrum Juelich GmbH
52425 Juelich
Sitz der Gesellschaft: Juelich
Eingetragen im Handelsregister des Amtsgerichts Dueren Nr. HR B 3498
Vorsitzender des Aufsichtsrats: MinDir Volker Rieke
Geschaeftsfuehrung: Prof. Dr.-Ing. Wolfgang Marquardt (Vorsitzender),
Karsten Beneke (stellv. Vorsitzender), Prof. Dr.-Ing. Harald Bolt
------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------
**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Kolloquium
*
*
*
**********************************************************************
Zeit: Mittwoch, 24. Februar 2021, 16:15-17:00 Uhr
Ort:
https://rwth.zoom.us/j/98137553896?pwd=WmVnYmhKdXhrM0hjS3NvQy84SjcwUT09
Meeting ID: 981 3755 3896
Passcode: 395762
**********************************************************************
Vortragende: Christina Büsing (RWTH)
Titel: Operational Planning for Mobile Medical Units
Abstract:
Mobile medical units allow for an efficient medical coverage of sparsely populated, spacious areas. Unfortunately, flexibility comes at the price of a highly complex operation planning process.
We developed a multi-staged optimization approach for the operation of mobile medical units combining facility location, scheduling and routing problems.
To determine our vehicle routes, we have to solve a budgeted matching problem on an edge colored graph, which we refer to as budgeted colored matching problem (BCM). We show the strong NP-hardness of the BCM on bipartite graphs with uniform edge weights, costs and budgets using a reduction from (3,B2)-SAT.
On special graph classes, the BCM is solvable in pseudo-polynomial time.
Finally, we evaluate the usage of mobile medical units in our model region situated in the northern Eifel. To assess the quality of solutions, we developed an agent-based simulation, which models the interaction between patients and general practitioners.
Es laden ein: die Dozentinnen und Dozenten der Informatik
**********************************************************************
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Donnerstag, 18. Februar 2021, 11:00-12:00 Uhr
Zoom:
https://rwth.zoom.us/j/92762889185?pwd=ZVdJV2o1bk13SlJCSDFRanB2TEYwUT09
Meeting-ID: 927 6288 9185
Kenncode: 725212
Referentin: Frau Sarah Suleri, M. Sc.
Lehrstuhl Informatik 5
Thema: Impact of Technological Support on the Workload of Software
Prototyping
Abstract:
Prototyping is a broadly utilized iterative technique for brainstorming,
communicating, and evaluating user interface (UI) designs. This research
aims to analyze this process from three aspects: traditional UI prototyping,
rapid prototyping, and prototyping for accessibility. We propose three novel
approaches and realize them by introducing three artifacts: 1) Eve, a
sketch-based prototyping workbench that supports automation of transforming
low fidelity prototypes to higher fidelities, 2) Kiwi, a UI design pattern
and guidelines library to support UI design pattern-driven prototyping, 3)
Personify, a persona-based UI design guidelines library for accessible UI
prototyping. We evaluate the usability of these artifacts, and the results
indicate good usability and learnability. Furthermore, we use NASA-TLX to
study the impact of using these three novel approaches on the subjective
workload experienced by the designers during the software prototyping
process. This work aims to extend prior work on UI prototyping and is
broadly applicable to understand the impact of using deep learning, UI
design patterns, and personas on the workload of UI prototyping.
Es laden ein: die Dozentinnen und Dozenten der Informatik
_______________________________
Leany Maaßen
RWTH Aachen University
Lehrstuhl Informatik 5, LuFG Informatik 5
Prof. Dr. Stefan Decker, Prof. Dr. Matthias Jarke,
Prof. Gerhard Lakemeyer Ph.D.
Ahornstrasse 55
D-52074 Aachen
Tel: 0241-80-21509
Fax: 0241-80-22321
E-Mail: maassen(a)dbis.rwth-aachen.de
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Mittwoch, 24. Februar 2021, 15:00-16:00 Uhr
Zoom:
<https://rwth.zoom.us/j/95286199371?pwd=M3hCUWk3VER6WnE0RlZzQUFBVFMzdz09>
https://rwth.zoom.us/j/95286199371?pwd=M3hCUWk3VER6WnE0RlZzQUFBVFMzdz09
Meeting-ID: 952 8619 9371
Kenncode: 424815
Referent: Herr Gustavo Alejandro Aragón Cabrera, M. Sc.
Lehrstuhl Informatik 5
Thema: Extended Model Predictive Control Software Framework for
Real-Time Local Management of Complex Energy Systems
Abstract:
Regarding the requirements of the future electrical grid due to high share
of renewable distributed generation, smart energy management systems (EMS)
are necessary to integrate the rapid development of ICT technologies and new
sensor and actuator technologies. This thesis deals with the challenges of
Model Predictive Control (MPC)-based EMS and introduces the concept of
extended MPC framework that includes ICT aspects of the integration of new
sensor and actuator technologies, forecasting methods, data management,
flexible optimization model definition and solvers integration in
consideration of user needs and deployment requirements in real systems. The
extended MPC framework is validated through its deployment in three
different use cases: as discrete and stochastic MPC in real test sites and
linked to a power flow simulator.
Es laden ein: die Dozentinnen und Dozenten der Informatik
_______________________________
Leany Maaßen
RWTH Aachen University
Lehrstuhl Informatik 5, LuFG Informatik 5
Prof. Dr. Stefan Decker, Prof. Dr. Matthias Jarke,
Prof. Gerhard Lakemeyer Ph.D.
Ahornstrasse 55
D-52074 Aachen
Tel: 0241-80-21509
Fax: 0241-80-22321
E-Mail: maassen(a)dbis.rwth-aachen.de
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Donnerstag, 18. Februar 2021, 10:15 Uhr
Ort: Zoom Videokonferenz
Link:
https://rwth.zoom.us/j/96519556069?pwd=MUVqbXpvZE5XVXBSdDNHZW5LMmJpQT09
Meeting-ID: 965 1955 6069
Kenncode: 482378
Referent: Anton Pirogov, M.Sc.
Lehrstuhl Informatik 7
Thema: Determinization and Ambiguity of Classical and Probabilistic
Büchi Automata
Abstract:
Büchi automata can be seen as a straight-forward generalization of
ordinary NFA,
adapted to handle infinite words. While they were originally introduced for
applications in decidability of logics, they became a popular tool for
practical
applications, e.g. in automata-based approaches to model checking and
synthesis
problems. Being arguably both the simplest and most well-known variant
in the
zoo of so-called omega-automata that are considered in this setting, they
serve as an intermediate representation of omega-regular specifications of
verification or synthesis requirements that are usually expressed in a more
declarative fashion, e.g. using linear temporal logic.
Unfortunately, nondeterministic automata are not directly suitable for
certain
applications, whereas deterministic Büchi automata are less expressive. This
problem is usually solved by either constructing deterministic automata of a
different kind, or by restricting their ambiguity, i.e., the maximal
number of
accepting runs on some word. In both cases, the transformation is expensive,
yielding an exponential blow-up of the state space in the worst case.
Therefore,
optimized constructions and heuristics for common special cases are
useful and
in demand for actual practical applications.
In this talk we present a new general construction for determinization from
nondeterministic Büchi to deterministic parity automata that unifies the
dominant branches of previous approaches based on the Safra construction
and the
Muller-Schupp construction. Additionally, we sketch a number of new
heuristics
for determinization, some of which exploit properties of our unified
construction.
Apart from the classical nondeterministic and deterministic variants of
automata, it is natural to consider probabilistic automata, i.e.,
automata that
use a probability distribution on the states instead of nondeterminism
to decide
which state to go to next. It is known that in general, such automata
are more
expressive than classical automata and many decision problems are
undecidable.
We present subclasses of probabilistic automata that correspond to certain
ambiguity classes and are not more expressive than classical automata.
Es laden ein: die Dozentinnen und Dozenten der Informatik
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Mittwoch, 10. Februar 2021, 14.00 Uhr
Zoom: https://rwth.zoom.us/j/91716576115?pwd=ZzUwemxXWUJkQURjQjJibmlGb3dYZz09
Meeting ID: 917 1657 6115
Passcode: 496556
Referent: Konrad Anton Fögen M.Sc.
Lehr- und Forschungsgebiet Softwarekonstruktion
Thema: Combinatorial Robustness Testing based on Error-Constraints
Abstract:
In this talk, we present an extension to combinatorial testing (CT) which is an effective specification-based test method that is based on an input parameter model (IPM). We argue that robustness is an important property of a software, which must be tested in addition to a software's functionality. This requires invalid values and invalid value combinations to be able to observe a software's reaction to them.
However, the effectiveness of CT deteriorates in the presence of invalid values or invalid value combinations. This phenomenon is called invalid input masking effect and is already acknowledged in some research. It led to extensions of CT that we call combinatorial robustness testing (CRT). The objective of CRT is to improve the fault detection by avoiding invalid input masking. This is achieved by separating the testing of valid values and valid value combinations from the testing of invalid values and invalid value combinations.
While CRT is a promising extension of CT, it is still insufficiently researched. For instance, in related work, IPMs are extended with additional semantic information to specify invalid values. However, invalid value combinations cannot be specified directly.
Therefore, the objective of this work is to further expand the idea of CRT. The aim is to develop a new CRT test method with a modeling approach to specify invalid values and invalid value combinations equally well. This modeling approach should also be incorporated into explicit test adequate criteria and test selection strategies. Furthermore, this modeling approach shall be supported by automated techniques.
First, we conduct a controlled experiment to check if CRT is necessary at all or if CT is already appropriate to test robustness. Based on the result, we continue and develop a refined t-factor fault model that incorporates robustness faults and the inherent invalid input masking effect.
Next, we develop a new test method for CRT and introduce a new structure that extends the structure of IPMs. It is called robustness input parameter model (RIPM) and contains the concept of error-constraints which is an additional set of logical expressions to describe the validity of values and value combinations.
With the refined t-factor fault model and the new RIPM structure, new test adequacy criteria that incorporate the additional semantic information and new test selection strategies that satisfy the test adequacy criteria are developed.
The new concept of error-constraints requires additional effort in modeling. Therefore, we develop two techniques to support the modeling of them. First, we develop a technique to identify and repair inconsistencies among error-constraints. Second, we develop a technique to automatically generate error-constraints based on the conformance to another system.
Last but not least, all aforementioned concepts and techniques are operationalized and integrated in a test automation framework which includes a process, an architecture, and a Java-based reference implementation.
Es laden ein: die Dozentinnen und Dozenten der Informatik
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Mittwoch, 10. Februar 2021, 15.00 Uhr
Zoom: https://rwth.zoom.us/j/96367107600?pwd=c2lMb2M1OXZXSHZFalRySUR2QTExUT09
Referent: Oliver Kautz M.Sc.
Lehrstuhl Informatik 3
Thema: Model Analyses Based on Semantic Differencing and Automatic Model Repair
Abstract:
Models are the primary development artifacts used in model-driven software development.
Therefore, models continuously evolve during the design, development, and
maintenance of software systems. Thus, model differencing is an important task to
understand the syntactic and semantic differences between model versions.
Previous work produced general (and thus language-independent) approaches for syntactic
model differencing, but only a few language-dependent approaches for semantic
model differencing. Approaches combining syntactic with semantic model differencing
by relating the syntactic changes of models to their semantic differences rarely exist.
Previous work neglected the development of language-independent approaches abstracting
from a concrete model property for detecting the syntactic elements of a model,
which cause that the model does not satisfy the property. If the property encodes a
requirement and the non-satisfaction represents the existence of a bug, then detecting
the syntactic model elements causing the non-satisfaction of the property facilitates
developers in detecting the syntactic model elements causing the bug.
In this talk, we present a framework for precisely defining modeling languages, including
syntax, semantics, and model evolution possibilities. We discuss syntactic and semantic
model differencing. The framework is instantiated with four concrete modeling languages:
Time-synchronous port automata, feature diagrams, sequence diagrams, and activity diagrams.
Based on the framework for precisely defining modeling languages, we present a modeling
language and property-independent framework for automatic model repairs. The framework
facilitates developers in detecting the syntactic elements of a model causing that the
model does not satisfy a property. Instantiating the framework with a concrete modeling
language and a concrete model property enables the automatic calculation of syntactic
changes that transform a model not satisfying the property to a model that satisfies the
property. The framework relies on the assumption that it is possible to partition the
syntactic changes applicable to each model into finitely many model-specific and property-
specific equivalence classes.
Es laden ein: die Dozentinnen und Dozenten der Informatik
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Freitag, 29. Januar 2021, 14.00 Uhr
Zoom: https://rwth.zoom.us/j/95719946489?pwd=S0lITm9pcW45b1k4SW5EVis2a1poQT09
Referent: Martin Serror, M.Sc.
Lehrstuhl Informatik 4
Thema: On the Benefits of Cooperation for Dependable Wireless Communications
Abstract:
The emerging Industrial Internet-of-Things (IIoT) improves flexibility, productivity, and costs
of industrial processes by connecting sensors, actuators, and controllers to each other and
the Internet. On the factory floor, such interconnections increasingly rely on wireless
communications, reducing deployment and maintenance costs while supporting the mobility
of communication partners. The industrial domain, however, is mainly characterized by safety-
and mission-critical Machine-to-Machine communication. Therefore, state-of-the-art wireless
communication protocols for home and business environments, such as WLAN and Bluetooth,
are not suited for the IIoT. Consequently, the IIoT requires dependable wireless communication,
achieving both high reliability and low latency.
A promising approach for so-called Ultra-Reliable Low-Latency Communication (URLLC) in the
IIoT is cooperative diversity, since the participating stations already collaborate toward a common
goal, i. e., keeping the industrial process running. There, a sending station exploits multiple
independent transmission paths via cooperating relays to convey a packet to its destination
reliably. In contrast to spatial diversity, this approach also works with single-input single-output
transceivers. However, when considering relaying for URLLC, it is particularly challenging that all
participants have to share the scarce transmission resources.
Hence, in this talk, we investigate various mechanisms enabling dependable wireless communication,
i. e., increasing communication reliability within a bounded low latency, where we mainly focus on the
benefits of cooperative diversity. Therefore, we explore different design options for URLLC and
evaluate them, leveraging the advantages of different methodological approaches. This talk thus offers
valuable insights into designing communication protocols with challenging requirements.
At the example of cooperation, we thoroughly retrace the development process from analysis to
prototypical deployment. On the one hand, the achieved results contribute to URLLC for the IIoT;
on the other hand, they provide a critical examination of the selected evaluation methodologies.
Es laden ein: die Dozentinnen und Dozenten der Informatik