Modul
Formale Systeme [M-INFO-100799]
Leistungspunkte
6Turnus
Jedes WintersemesterDauer
1 SemesterSprache
DeutschLevel
3Version
1Verantwortung
Einrichtung
- KIT-Fakultät für Informatik
Bestandteil von
Teilleistungen
Identifier | Name | LP |
---|---|---|
T-INFO-101336 | Formale Systeme | 6 |
Erfolgskontrolle(n)
Siehe Teilleistung.
Qualifikationsziele
Nach Abschluss des Moduls verfügen Studierende über folgende Kompetenzen. Sie …
- kennen und verstehen die vorgestellten logischen Grundkonzepte und Begriffe, insbesondere den Modellbegriff und die Unterscheidung von Syntax und Semantik,
- können natürlichsprachlich gegebene Sachverhalte in verschiedenen Logiken formalisieren sowie logische Formeln verstehen und ihre Bedeutung in natürliche Sprache übersetzen,
- können die vorgestellten Kalküle und Analyseverfahren auf gegebene Fragestellungen bzw. Probleme sowohl manuell als auch mittels interaktiver und automatischer Werkzeugunterstützung anwenden,
- kennen die grundlegenden Konzepte und Methoden der formalen Modellierung und Verifikation,
- können Programmeigenschaften in formalen Spezifikationssprachen formulieren, und kleine Beispiele mit Unterstützung von Softwarewerkzeugen verifizieren.
- können beurteilen, welcher logische Formalismus und welcher Kalkül sich zur Formalisierung und zum Beweis eines Sachverhalts eignet
Voraussetzungen
Siehe Teilleistung.
Inhalt
Logikbasierte Methoden spielen in der Informatik in zwei Bereichen eine wesentliche Rolle: (1) zur Entwicklung, Beschreibung und Analyse von IT-Systemen und (2) als Komponente von IT-Systemen, die diesen die Fähigkeit verleiht, die umgebende Welt zu analysieren und Wissen darüber abzuleiten.
Dieses Modul
- führt in die Grundlagen formaler Logik ein und
- behandelt die Anwendung logikbasierter Methoden
- zur Modellierung und Formalisierung
- zur Ableitung (Deduktion),
- zum Beweisen und Analysieren
von Systemen und Strukturen bzw. deren Eigenschaften.
Mehrere verschiedene Logiken werden vorgestellt, ihre Syntax und Semantik besprochen sowie dazugehörige Kalküle und andere Analyseverfahren eingeführt. Zu den behandelten Logiken zählen insbesondere die klassische Aussagen- und Prädikatenlogik sowie Temporallogiken wie LTL oder CTL.
Die Frage der praktischen Anwendbarkeit der vorgestellten Logiken und Kalküle auf Probleme der Informatik spielt in dieser Vorlesung eine wichtige Rolle. Der Praxisbezug wird insbesondere auch durch praktische Übungen (Praxisaufgaben) hergestellt, im Rahmen derer Studierende die Anwendung aktueller Werkzeuge (z.B. des interaktiven Beweisers KeY) auf praxisrelevante Problemstellungen (z.B. den Nachweis von Programmeigenschaften) erproben können.
Empfehlungen
Siehe Teilleistungen.
Arbeitsaufwand
Der Gesamtarbeitsaufwand für dieses Modul beträgt 180h.
Der Aufwand setzt sich zusammen aus:
34,5h = 23 * 1,5hVorlesung (Präsenz)
10,5h = 7 * 1,5h Übungen (Präsenz)
60h Vor- und Nachbereitung, insbes. Bearbeitung der Übungsblätter
40h Bearbeitung der Praxisaufgaben
35h Klausurvorbereitung