+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Dienstag, 15.02.2022, 13:00-14:00 Uhr
Zoom:
<https://rwth.zoom.us/j/95759728127?pwd=RFhzRTh1STJYTXZyanVIdWYweVkwZz09>
https://rwth.zoom.us/j/95759728127?pwd=RFhzRTh1STJYTXZyanVIdWYweVkwZz09
Meeting-ID: 957 5972 8127
Kenncode: 112136
Referent: Herr Vinoth Sermuga Pandian, M.Sc.
Lehrstuhl Informatik 5
Thema: BlackBox Toolkit: Intelligent Assistance to UI Design
Abstract:
This dissertation conducts systematic research using a human-centred
approach to provide Artificial Intelligence (AI) assistance to User
Interface (UI) designers before, during, and after the traditional low
fidelity (LoFi) prototyping process. As a result, it aims to provide
coherent AI assistance throughout the repetitive and arduous LoFi
prototyping task without sacrificing the autonomy of UI designers. In doing
so, we contribute the BlackBox Toolkit. This toolkit assists designers by
creating four large-scale, diverse, open-access benchmark datasets and three
AI tools that assist UI designers throughout the LoFi prototyping process.
The quantitative and qualitative evaluation of the AI tools shows that the
UI designers perceive utilising AI for UI design as a novel and helpful
approach and express their willingness to adopt it. The After Scenario
Questionnaire study to measure designer satisfaction results show an
above-average satisfaction level for all three AI assistance tools. This
research aims to understand the impact of AI tools in UI designer workflow
and assess their satisfaction upon using these AI tools. Further, it sets a
baseline for future research on UI wireframe generation, refinement and
transformation.
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: Freitag, 4. Februar 2022, 15.00 Uhr
Ort: Zoom-Videokonferenz (https://rwth.zoom.us/j/98899850408?pwd=VTJWdUg2ZDUwK21mU2haa01HdEdIQT09)
Referent: Nadja Zaric, M.Sc.
Lehr- und Forschungsgebiet Informatik 9
Thema: PEGAM - a Personalized Gamification design Model for programming language e-courses
Abstract:
This dissertation addresses low academic participation and engagement as issues often related to students' retention in online learning courses. The issues were identified at the Department of Computer Science at RWTH Aachen University, Germany, although high dropout rates are a growing problem in Computer Science studies worldwide.
A solving approach often used in addressing the beforementioned problems includes gamification and personalization techniques: Gamification is a process of applying game design principles in serious contexts (i.e., learning), while personalization refers to tailoring the context to users' needs and characteristics. In this work, the two techniques are used in combination in the Personalized Gamification Model (PeGaM), created to design an online course for learning programming languages.
PeGaM is theoretically grounded in the principles of the Gamified Learning Theory and the theory of learning tendencies. Learning tendencies define learners' preferences for a particular form of behavior, and those behaviors are seen as possible moderators of gamification success. Moderators are a concept explained in the Gamified Learning Theory, and refer to variables that can influence the impact of gamification on the targeted outcomes. Gamification success is a measure of the extent to which students behave in a manner that leads to successful learning. The conceptual model of PeGaM is an iterative process in which learning tendencies are used to identify students who are believed to be prone to avoid certain activities. Gamification is then incorporated in activities that are recognized as 'likely to be avoided' to produce a specific learning-related behavior responsible for a particular learning outcome. PeGaM model includes five conceptual steps and 19 design principles required for gamification of learning environments that facilitate student engagement and participation.
In practice, PeGaM was applied in an introductory JavaScript course with Bachelor students of Computer Science at RWTH Aachen University. The investigation was guided by the principles of the Design-Based Research approach. Through this approach, PeGaM was created, evaluated and revised, over three iterative cycles. The first cycle had an explorative character, included one control and one treatment group, and gathered 124 participants. The second and third cycles were experimental studies, in which 69 and 171 participants were randomly distributed along with one control and two treatment groups. Through the three interventions, mixed methods were used to capture students' academic participation (a measure of students' online behavior in the course collected through activity logs), engagement (evaluated quantitatively through a questionnaire compiled to measure behavioral, emotional, and cognitive engagement), and gameful experience (quantitative measure of students' experience with the gamified system). In addition, supporting data was collected through semi-structured interviews and open-ended survey questions.
The empirical findings revealed that gamification with PeGaM contributes to learning outcomes and that the success of gamification is conditioned by the applicability of game elements with learners' preferences and learning activities. Cross case comparisons supported the application of PeGaM design principles and demonstrated its potential. Even though limited support was found to confirm the moderating role of learners' learning tendencies, the study demonstrated that the gamification of learning activities that students are likely to avoid can increase their participation - but must be carefully designed. Most importantly, educational gamification can support and enhance learning-related behavior but require relevant and meaningful learning activities in combination with carefully considered reward, collaborative and feedback mechanisms.
The study provides practical and theoretical insights but also highlights challenges and limitations associated with personalized gamification thus offering suggestions for further investigation.
Es laden ein: die Dozentinnen und Dozenten der Informatik
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Montag, 13. Dezember 2021, 11:00 Uhr
Ort: Videokonferenz (Zoom-Meeting, Informationen siehe unten)
Referent: Stefan Kühnel, Dipl. Wirt.-Inf.
Informatik 3 - Software Engineering
Thema: Eine agile Methode zur simulativen Qualitätssicherung von Aktiven
Sicherheitssystemen
Kontext: Neben dem aktuellen Bestreben die Elektrizierung des Antriebs
von Automobilen durch Innovationen voranzutreiben kommt der Integration
von Fahrerassistenzsystemen im Rahmen der Automobilentwicklung eine
besondere Bedeutung sowohl zur Steigerung des Fahrkomforts als auch zur
Verbesserung der Sicherheit zu. Eine gewichtige Rolle spielen dabei
Consumer Tests wie z.B. von Organisationen wie EuroNCAP, welche sowohl
als Treiber aber auch zur Beurteilung der Leistungsfähigkeit der
getesteten Sicherheitssysteme dient. Um die Qualität der dafür
entwickelten Software besser beurteilen und steigern zu können, bilden
Tests sowohl in ausgewiesenen Prüfarealen unter realen Bedingungen als
auch simulationsbasierte Tests in synthetischen Umgebungen geeignete
Ansätze, den Herausforderungen der kontinuierlichen
Qualitätsverbesserung agil zu begegnen, wenngleich beide Ansätze über
unterschiedliche Hürden und Grenzen verfügen. Speziell der hier
betrachtete simulative Ansatz mündet nicht selten in dem Dilemma, dass
die Entwicklung geeigneter Umgebungen ebenfalls ein hohes Maß an
Ressourcen wie die eigentliche Systementwicklung benötigt und somit
Letztere weiter parallel voranschreitet mit der Folge, dass die
Simulationsumgebung aufgrund des hohen Aufwandes nicht rechtzeitig
einsetzbar ist. Dies kann dann bspw. eintreten, wenn dem Aspekt der
Modellbildung mit dem Güteziel einer möglichst engen Realitätsnähe ohne
Rückkopplung auf die eingangs zu definierende Fragestellung: “Was soll
durch die Simulation beantwortet werden?” erfolgt.
Ziel: Das Ziel dieser Arbeit besteht darin, den komplexen
Entwicklungsprozess von Aktiven Sicherheitssystemen im Rahmen der
Consumer Tests durch einen simulativen Ansatz zur Verbesserung der
Softwarequalität zu unterstützen. Weiterhin soll durch die
Verhaltensanalyse von Algorithmen die Ressourcenallokation während der
Entwicklung und der notwendigen realen Tests verbessert und damit
effektiver gestaltet werden.
Methode: Nach der Durchführung eines Systematic Literature Reviews (SLR)
zu Prüfung evtl. vorhandener Ansätze und Methoden zur Entwicklung
solcher Simulationsumgebungen wird eine eigene Methode entwickelt,
vorgestellt und unter Berücksichtigung der vorliegenden
Projektbedingungen diese Methode im Rahmen einer Fallstudie angewendet.
Ergebnisse: Die Analyse des Projektkontextes kommt zu dem Ergebnis, dass
es durchaus Simulationsaktivitäten gibt, jedoch eine strukturierte
Herangehensweise zu ihrer Entwicklung fehlt. Das Systematic Literature
Review bestätigt dieses Ergebnis, sodass der Bedarf der Entwicklung
einer agilen Methode zur simulativen Qualitätssicherung von Aktiven
Sicherheitssystemen insbesondere mit Blick auf Consumer Tests aufgezeigt
wird. Die vorgestellte Methode umfasst vier Bausteine: (a) die Analyse
und Modellierung des Untersuchungsraumes, (b) die Entwicklung einer
adäquaten Simulationsinfrastruktur, (c) die Entwicklung von
Bewertungsverfahren und (d) die Durchführung von Simulationsläufen sowie
ihrer Auswertung. Zum Schluss wird die Methode mit Hilfe einer
Fallstudie für ein Proof of Concept angewendet.
Schlussfolgerung: Es wird aufgezeigt, dass die Methode während der
qualitativen Bewertung von Softwarekomponenten auf simulativer Basis
einen positiven Beitrag leistet, speziell dort, wo
Äquivalenzklassentests nicht ausreichend sind, Consumer Test Szenarien
hinreichend zu testen. Einschränkungen und Erweiterungsbedarf der
Methode werden vorrangig in der Übertragung auf andere Kontexte im
Fahrerassistenzumfeld und die Erweiterung um zusätzliche Consumer Test
Szenarien wie den Fußgängerschutz gesehen.
Es laden ein: die Dozentinnen und Dozenten der Informatik
********************************
Thema: [Promotion Stefan Kühnel] Vortrag
Uhrzeit: 13. Nov. 2021 11:00 AM Amsterdam, Berlin, Rom, Stockholm, Wien
Zoom-Meeting beitreten
https://rwth.zoom.us/j/98203910423?pwd=UlRyWFNFSXpaNzZnQm9oZEE5T3lpZz09
Beste Grüße, Stefan Kühnel
--
----------------------------------------------------------------
Prof. Dr. Bernhard Rumpe | http://www.se-rwth.de
Lehrstuhl Software Engineering | Informatik 3
Ahornstr. 55, 52074 Aachen, Germany | RWTH Aachen University
Phone ++49 241 80-21301 / Fax -22218 |
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Montag, 13. Dezember 2021, 11.00 Uhr
Ort: Zoom-Videokonferenz
https://rwth.zoom.us/j/93783577046?pwd=NjFUNFZZUWpzNjhLN2VlOHEyVk9nQT09
Meeting-ID: 937 8357 7046
Kenncode: 561405
Referent: Jens Deussen M.Sc.
Lehrstuhl Informatik 12: Software and Tools for
Computational Engineering
Thema: Global Derivatives
Abstract:
In this talk, we show how to obtain global derivatives that are
guaranteed enclosures of the derivative information on specified
domains. Therefore, we combine algorithmic differentiation (AD) methods
with interval arithmetic and McCormick relaxations. While naive interval
computations are prone to overestimation of exact value ranges, we
identify special cases for which the natural interval extension applied
to the AD methods compute exact value ranges for the global derivatives.
We present two applications that benefit from global derivatives:
deterministic global optimization by branch-and-bound methods, and
significance-driven unreliable and approximate computing. Within the
framework of the global optimization case study we introduce subdomain
separability. This local property enables the partitioning of the
optimization problem on subdomains that fulfill a certain monotonicity
condition. The approximate computing case study demonstrates how to
automatically prune artificial neural networks by using significance values.
Es laden ein: die Dozentinnen und Dozenten der Informatik
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Freitag, 03. Dezember 2021, 10.00 Uhr
Ort: Zoom Videokonferenz
https://us02web.zoom.us/j/88210359250?pwd=QXFGMUEzTGRDVmJBbHgwT0lXcEhrdz09
Meeting-ID: 882 1035 9250
Kenncode: 542690
Referent: Lucas Beyer, Dipl.Ing
Lehrstuhl Informatik 13
Thema: Deep Visual Human Sensing with Application in Robotics
Abstract:
In this talk, I present my thesis contributions to the field of visual
human sensing that arise when deploying robots in environments with humans.
After motivating the need for visual human sensing, we start by describing
a novel human detector based on a 2D lidar sensor (e.g. a "laser scanner").
It is the first of its kind that is learning-based and general,
specifically it does not encode a "two leg prior".
Detection being covered, we move on to discuss person re-identification,
and specifically our contribution of establishing triplet-loss based
methods as a strong contender and principled approach in the field. Using
this we also sketch the way to a completely novel approach on tracking
which leverages such triplet-based re-identification models at its core.
We then discuss more detailed analysis of individual persons, specifically
their head orientation, which can serve as a cue for their intent or an
indicator of what is interesting in the scene, among other things. We
derive a novel cyclic regression loss based on the von-Mises distribution
and use it, coupled with our "biternion" output layer, to learn continuous
regression models using only discrete, weakly labeled data.
Finally, we present a holistic system integrating all of these pieces and
several more, highlighting the system-level difficulties of such
integration, and proposing some ways around them.
Es laden ein: die Dozentinnen und Dozenten der Informatik
***********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Kolloquium
*
*
*
***********************************************************************
Zeit: Mittwoch, 1. Dezember 2021, 13.30 Uhr
Ort: Zoom Videokonferenz
https://rwth.zoom.us/j/95857189087?pwd=ajNJYUZFcHVvSHNFUmJya1RqUFhKUT09
Meeting-ID: 958 5718 9087
Kenncode: 050524
Referent: Christopher Morris, Quebec AI Institute and McGill University
Thema: Learning with Graphs: From Theory to Applications
Abstract:
Graph-structured data is ubiquitous across domains ranging from chemo- and bioinformatics to image and social network analysis. To develop successful machine learning models in these domains, we need techniques mapping the graph's structure to a vectorial representation in a meaningful way---so-called graph embeddings. Starting from the 1960s in chemoinformatics, different research communities have worked in the area under various guises, often leading to recurring ideas. Moreover, triggered by the resurgence of (deep) neural networks, there is an ongoing trend in the machine learning community to design permutation-invariant or -equivariant neural architectures capable of dealing with graph input often denoted as neural graph networks (GNNs). However, although often successful in practice, GNN's capabilities and limits are understood to a lesser extend. In this talk, we overview some results shedding some light on the limitations and capabilities of GNNs by leveraging tools from graph theory and related areas. To complement the theory, we show how GNNs can act as an inductive bias to enhance state-of-art solvers for combinatorial optimization in a data-driven way.
Es laden ein: die Dozentinnen und Dozenten der Informatik
—
Martin Grohe
RWTH Aachen
Lehrstuhl Informatik 7
Ahornstr. 55
52074 Aachen
Germany
e: grohe(a)informatik.rwth-aachen.de
t: +49 241 80 21700
f: +49 241 8022 215
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Montag, 29. November 2021, 14.00 Uhr
Ort: Zoom Videokonferenz
https://rwth.zoom.us/j/93845227037?pwd=cm9qRjhtVm5JbWRYdGkrSUsyRythdz09
<https://www.google.com/url?q=https://rwth.zoom.us/j/93845227037?pwd%3Dcm9qR…>
Meeting ID: 938 4522 7037
Passcode: 310833
Referent: Theodora Kontogianni, M.Sc.
Lehrstuhl Informatik 13
Thema: Object Discovery, Interactive and 3D Segmentation for Large-Scale
Computer Vision Tasks
Abstract:
In this talk, I present my thesis contributions that deal with issues
arising when trying to exploit the large body of data available for
computer vision tasks.
In particular we address the problem of unsupervised object discovery in
time-varying, large-scale image collections by proposing a novel tree
structure that closely approximates
the Minimum Spanning Tree and present an efficient construction approach
along with an incremental update mechanism of the tree structure that
incorporates new data as they are added to the image database.
We then focus on defining novel 3D convolutional and recurrent operators
over unstructured 3D point clouds. The goal is to learn point
representations for the task of 3D semantic segmentation. We overcome the
limitations of the unstructured and large-scale nature of the 3D point
clouds by defining local structure through two clustering methods and
expand the limited receptive field of previous approaches by modeling
long-range relationships with the use of Recurrent Networks.
In the third part, we address the task of interactive object segmentation
where a computer vision algorithm segments an object aided by a human user.
We present a method that significantly reduces the number of required user
clicks compared to previous works. We use the sparse user corrections to
adapt the model parameter on-the-fly during test time. In particular, we
look at out-of-domain settings where the test datasets are significantly
different from the datasets used to train our deep learning model.
Es laden ein: die Dozentinnen und Dozenten der Informatik
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Montag, 22. November 2021, 10:00-11:00 Uhr
Zoom:
https://rwth.zoom.us/j/95217813154?pwd=RkQ1ZTllbi94OUZiZDRNRE15eGpHZz09
Meeting ID: 952 1781 3154
Passcode: 596536
Referent: Herr Dipl.-Inform. Martin Liebenberg
LuFG Informatik 5
Thema: Autonomous Agents for the World Wide Lab Artificial
Intelligence in the Manufacturing Industry
Abstract:
The Internet of Production (IoP) is a research programme, where 30
interdisciplinary institutes work on revolutionising the manufacturing
industry. A central concept of the IoP is the World Wide Lab (WWL) by which
in a lab of labs the data of many manufacturing processes should be made
available as if the data came from ones own manufacturing processes. With
this data, which we receive from the WWL, we want to build Digital Shadows
that are condensed or aggregated data for a specific purpose, such as a
reduced mathematical model or a trained neural network. An early vision of
the usage of the IoP is a Google-like web search, where one can pose a
manufacturing problem and get in return an answer with which one can improve
ones production process or build new products.
In my thesis, I propose a solution to realise such a scenario based on
Artificial Intelligence (AI) methods, which I call WWL Agents. Inspired by
the ideas of the Semantic Web, these agents should automate the search for
data, knowledge or Digital Shadows in the WWL for specific manufacturing
problems, which we think is impractical to do manually. Furthermore, WWL
Agents should apply the found information to build Digital Shadows or
improve manufacturing processes.
In this talk, we present the development of WWL Agents from three different
perspectives. First, we consider it from the perspective of building Digital
Shadows in a cross-domain collaboration. The second perspective relates to
modelling the behaviour of WWL agents. Finally, we discuss the
infrastructure required by a WWL Agent to provide semantic interoperability
in the WWL. By these means we obtain a powerful concept by which the user
can get the precise meaning of an answer and, through provenance
information, knowledge about the origin of entities of the answer. Moreover,
we demonstrate applications for WWL Agents in manufacturing in one exemplary
use case where the agents plan production processes. In hot rolling, we show
that, with local search, agents can find very quickly schedules, which could
be used to repair failed rolling schedules during operation.
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: Montag, 4. Oktober 2021, 10.00 Uhr
Ort: Zoom-Videokonferenz (https://rwth.zoom.us/j/93693721093?pwd=OWo0eXJaajgram9lY1hxUVE1N0lXZz09)
Referent: Svenja Noichl M.Sc.
Lehr- und Forschungsgebiet Informatik 9
Thema: InfoBiTS: Informatische Bildung für Technikferne Seniorinnen und Senioren
Abstract:
Digitale Kompetenzen gewinnen im Zuge der fortschreitenden Digitalisierung in allen Bereichen des alltäglichen Lebens zunehmend an Relevanz. Dies gilt auch für ältere Personen, welche bisher wenig oder keine Berührungspunkte mit digitalen Technologien hatten. Unter Digitalkompetenz oder digitaler Kompetenz wird hier die Kombination aus Medienkompetenz und Informatikkompetenz verstanden, also die Kombination aus Aspekten der Medienkunde, Medienkritik, Mediennutzung und Mediengestaltung sowie Grundkenntnissen über unter anderem die Funktionsweisen von Informatiksystemen. Während in bestehenden Angeboten für ältere Menschen, wie z. B. Computer-, Smartphone- oder Tabletkursen, bei Peer-Learning Angeboten oder bei Technikbegleitung und Sprechstunden, zumeist die Medienkompetenz adressiert wird, soll das hier entwickelte Angebot einen größeren Fokus auf die Informatikkompetenz legen. Durch die Vermittlung von Ideen und Konzepten aus der Informatik, soll so über die reine Nutzungskompetenz digitaler Endgeräte hinaus, übertragbares Wissen dieser Domäne gefördert werden. Die Zielgruppe sind Personen ab 50 Jahren, welche keine bis wenig Vorerfahrung mit digitalen Technologien besitzen. Um den Lernerfolg in dem für die Zielgruppe neuen Gebiet bestmöglich zu unterstützen, ist die Berücksichtigung der Geragogik unerlässlich. Drei wichtige Aspekte stellen hierbei (1) das Lernen mit Gleichgesinnten, (2) das Lernen in einem geschützten Raum sowie (3) schnelle Hilfe bei Fragen und Problemen dar. Das hier entwickelte Angebot setzt daher nicht auf eine alleinige Nutzung der entwickelten Lernapp (InfoBiTS), sondern bettet diese in ein Kurskonzept ein. Bewährt hat sich dafür ein Workshopsetting. Ein Onlinesetting ist mit Einschränkungen ebenfalls möglich. Die InfoBiTS-App beinhaltet vier Lernmodule, welche sich mit den Themen Kommunikation, Funktionsweise des Internets, mobile Geräte und das Internet sowie Datenschutz und Datensicherheit befassen. Die Module adressieren hierbei jeweils Kompetenzen aus dem Curriculum für Seniorinnen und Senioren, welches im Rahmen dieser Arbeit entwickelt wurde und auf nationalen und internationalen Schulcurricula sowie Interessen der Zielgruppe, welche in einem Fragebogen mit 123 Teilnehmenden erhoben wurden, basiert. Für die konkrete Themenauswahl waren darüber hinaus Themen aktueller Relevanz sowie Anknüpfungspunkte an den Alltag der Zielgruppe, z. B. die Kommunikation mit (entfernt lebenden) Kindern und Enkeln, maßgeblich. Während die Pilotstudie im Workshopsetting durchgeführt wurde, erfolgte die Evaluation, aufgrund der Einschränkungen durch die vom Coronavirus SARS-CoV-2 ausgelöste Pandemie, im Onlinesetting. Insgesamt nahmen 19 Personen zwischen 50 und 84 Jahren teil. Die Evaluation zeigte insbesondere, dass sich das Gefühl der Kontrolle im Umgang mit und über die Technik im Vergleich zu vor dem ersten Modul und nach dem letzten Modul signifikant verbesserte. Weiterhin deuten die Ergebnisse einer modulbezogenen Selbsteinschätzung sowie die Bearbeitung der Aufgaben innerhalb der Module darauf hin, dass die angestrebten Lernziele in den Modulen weitestgehend erreicht werden konnten, was auf eine Förderung der adressierten Kompetenzen aus dem Curriculum hindeutet. Letztlich weißt die Auswertung des DigComp 2.1, dem europäischen Referenzrahmen für digitale Kompetenzen, nicht nur auf eine Verbesserung der erwarteten Kompetenzen hin, sondern auch auf eine Verbesserung weiterer Kompetenzen, wie beispielsweise im Bereich des Umgangs mit technischen Problemen.
Es laden ein: die Dozentinnen und Dozenten der Informatik
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Donnerstag, 23. September 2021, 11.00 Uhr
Zoom: https://rwth.zoom.us/j/92021395779?pwd=ckRtKzJhcHFmeWxaU3YxSEZRWTJTUT09
Meeting-ID: 920 2139 5779
Kenncode: 534446
Referent: Dimitri Bohlender M.Sc.
Lehrstuhl Informatik 11
Thema: Symbolic Methods for Formal Verification of Industrial Control Software
Abstract:
Many of the systems that we rely on, and interact with on a daily basis, are driven by
software. Unfortunately, design and implementation of such systems is naturally prone to
error, as it is done by humans and involves reasoning about the vast number of states a
system may reach. While testing is the common approach to alleviating the risk of writing
faulty software, it can only help with finding errors, but not prove their absence.
By way of contrast, formal methods have mathematical foundations and enable rigorous
reasoning about the behaviour of formally modelled systems. In particular, they
give rise to formal verification procedures for proving a system's compliance with certain
formal specifications. Although many such procedures can simplistically be thought of
as an automatic exploration of a system's state space, the explicit enumeration of each
reachable state can often be avoided. To this end, symbolic methods reason about many
states at a time by representing sets of states and transition relations as logical formulas.
My thesis is concerned with advances in symbolic methods for formal verification of
the software-driven reactive systems that are used in the setting of industrial automation.
While these systems often operate in safety-critical environments, the specifications and
peculiarities of the domain impede the use of existing verification machinery for general-purpose
programming languages, leaving engineers in need of computer-aided reasoning
about the control software semantics. Our contributions address this issue in platform-agnostic
ways, but are presented using the example of programmable logic controllers
which are tailored to the industrial automation domain and therefore widely used.
In this talk, we give an overview over our contributions with a focus on the approaches
that leverage constrained Horn clause solving. After a short introduction, we sketch how
a logical characterisation of control software safety in terms of constrained Horn clauses
can be derived from reactive systems safety foundations. To exploit the modularity of
control software, the characterisation is also extended and combined with mode
abstraction – a domain-specific analysis for approximating the state space. Furthermore,
we present approaches for the design and verification of control software that is resilient
to potential restarts of the controller. We show how the choice of persistent variables can
be reduced to parameter synthesis, and solved by extending the previous verification procedures.
Es laden ein: die Dozent*innen der Informatik