Vorlesungen im Wintersemester 2023/24
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: Von der Theorie zur Anwendung
In diesem Seminar werden verschiedene formale Techniken vorgestellt, die dazu beitragen, Programme auf ihre Korrektheit überprüfen zu können. Einige Techniken stellen neue vielversprechende Ansätze vor, andere zeigen auf wie durch geschickten Einsatz und Kombination von Heuristiken existierende Ansätze um Größenordnungen leistungsfähiger gemacht werden können. Die vorgestellten Ansätze helfen praxisnah, Probleme in Software zu entdecken, zu vermeiden oder zu verhindern.
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)