Vorlesungen im Wintersemester 2024/25

Im Wintersemester finden am KASTEL-Institut eine Reihe von Vorlesungen zu verschiedenen Themen aus dem Gebiet der Formalen Methoden statt. Jede Veranstaltung hat ihren besonderen Schwerpunkt und diese Seite will Ihnen einen Überblick über das Angebot geben.

Das Stammmodul Formale Systeme liefert eine gute Basis für alle Veranstaltungen.

Im Institutsseminar gibt es auch eine Reihe an interessanten Vorträgen rund um formale Methoden.

Formale Systeme

Umfang:	4 SWS / 6 Leistungspunkte
	Stammvorlesung
Zeit:	Donnerstags 14:00-15:30, Freitags 11:30-13:00
Ort:	HS -101 50.34 (Do), Gaede-Hörsaal (Fr)
> > > > Link zur Vorlesung < < < <

Logical Foundations of Cyber-Physical Systems

Umfang:	3+1 SWS / 5 Leistungspunkte
Vertiefungsfächer:	Theoretische Grundlagen und Softwaretechnik und Übersetzerbau
Zeit:	Montags 09:45-11:15, Dienstags 11:30-13:00
Ort:	SR 301, Geb. 50.34
Bemerkungen:	Sprache englisch/deutsch
> > > > Link zur Vorlesung < < < <

Cyber-physical systems (CPSs) combine cyber capabilities (computation and/or communication) with physical capabilities (motion or other physical processes). Cars, aircraft, and robots are prime examples, because they move physically in space in a way that is determined by discrete computerized control algorithms. Designing these algorithms to control CPSs is challenging due to their tight coupling with physical behavior. At the same time, it is vital that these algorithms be correct, since we rely on CPSs for safety-critical tasks like keeping aircraft from colliding. In this course we will strive to answer the fundamental question posed by Jeannette Wing:
"How can we provide people with cyber-physical systems they can bet their lives on?"

Seminare

Neben den Vorlesungen gibt es auch Seminare, deren Inhalte sich (u.a.) mit der Anwendung Formaler Methoden in der Software-Entwicklung auseinandersetzen.

Anwendung Formaler Verifikation: Neuronale Netze in Formaler Verifikation

Ziel dieses Seminars ist es, einen Überblick über die aktuelle Forschungslandschaft im Bereich der formalen Verifikation und den Anwendungsbereich neuronaler Netze in diesem Bereich zu geben. Insbesondere werden die folgenden zwei Schlüsselaspekte untersucht:

1. Verifikation neuronaler Netze:
   Die Verifikation neuronaler Netze konzentriert sich auf die Techniken, Methoden und Werkzeuge, die sicherstellen, dass neuronale Netze sicher, zuverlässig und wie beabsichtigt funktionieren. Dazu gehört die Überprüfung der Genauigkeit, Robustheit und Erklärbarkeit der trainierten Modelle sowie deren sicherer Einsatz in Anwendungsplattformen.
2. Neuronale Netze für die Verifikation:
   Neuronale Netze für die Verifikation beinhalten die Nutzung von KI und maschinellen Lerntechniken, um traditionelle Verifikationsmethoden zu verbessern und sie für praktische Systeme skalierbarer, effizienter und effektiver zu machen.

Da KI ein immer wichtigeres Thema wird, sind diese beiden Forschungsrichtungen von großer Bedeutung: Einerseits können uns die exakten Techniken im Bereich der formalen Verifikation helfen, vertrauenswürdige KI-Systeme zu entwickeln, andererseits besteht die Hoffnung, dass KI uns helfen kann, die auf formalen Methoden basierende Analyse auf viel größere Systeme zu skalieren. Ziel des Seminars ist es, einen Überblick über dieses aufstrebende Forschungsgebiet zu geben und im Rahmen des Seminars die Diskussion über die vorgestellten Themen zu fördern.

Am Lehrstuhl "Anwendungsorientierte Formale Verifikation" (Prof. Beckert und Mitarbeiter:innen)

Applications and Extensions of Timed Systems

Many of the (embedded) software systems we are confronted with in everyday life have time-critical functionalities. For example, in the event of an accident, an airbag should be activated within a specific, very short, period of time. As another example: we expect fast response times from our smartphones so that we can use them conveniently and purposefully. When modeling software systems, "time" is therefore a decisive factor. In this seminar, various mechanisms to formalise and analyse so-called real-time systems are discussed. The lecture also focuses on applications of timed systems. For instance, the following topics are dealt with:

• Timed Games
• Applications of Timed Automata (e.g. UPPAAL in Space)
• Synthesising Strategies using UPPAAL Stratego
• Duration Calculus (e.g. Satisfiability, Calculus)
• Interval Temporal Logic vs Duration Calculus

The module will consist of an introductory lecture part, where some basic topics around timed systems are introduced. For the second half of the module, the students will prepare papers and topic talks each in teams of two students. Aditionally, a conference-style peer-review process for the papers is planned amongst the students. It is also expected that the students actively discuss their topics with their fellow students.

Am Lehrstuhl "Modellierung und Analyse im Mobility Software Engineering" (Jun.-Prof. Dr. Maike Schwammberger und Mitarbeiter:innen)

Praktikum

Forschungspraktikum im Rahmen der Vorlesung Formale Systeme

In diesem Semester bieten wir neben der Vorlesung ein optionales begleitendes Forschungspraktikum im Umfang von insgesamt fünf Leistpungspunkten (LP) (davon zwei Schlüsselqualifikation (SQ)) an. Hierbei handelt es sich um ein Projektpraktikum, in dem über das ganze Semester an einem Thema gearbeitet wird (und nicht an verschiedenen Aufgabenblättern). Die Bearbeitung aktueller Forschungsthemen erfordert hierbei ein größeres Maß an Eigeninitiative als dies bei im Vorhinein festgelegten Praktika der Fall ist. Die Fortschritte werden dabei regelmäßig mit einem bzw. einer betreuenden Mitarbeitenden der Forschungsgruppe diskutiert.

Am Lehrstuhl "Anwendungsorientierte Formale Verifikation" (Prof. Beckert und Mitarbeiter:innen)