Hier werden die Unterschiede zwischen zwei Versionen angezeigt.
| — | lehre:wise1819:formale_methoden_fuer_steuerungssoftware [2024/10/30 03:13] (aktuell) – angelegt - Externe Bearbeitung 127.0.0.1 | ||
|---|---|---|---|
| Zeile 1: | Zeile 1: | ||
| + | ====== Formale Methoden für Steuerungssoftware ====== | ||
| + | |||
| + | === Inhalt === | ||
| + | |||
| + | In dieser Vorlesung werden Grundlagen und Anwendungen von statischer Analyse und Model-Checking im Bereich Steuerungssoftware vermittelt. Dazu werden entsprechende Analysen und Algorithmen auf den zyklischen Betrieb von Speicherprogrammierbaren Steuerungen angepasst. Behandelte Themen sind u.A.:\\ | ||
| + | \\ | ||
| + | * Die Programmiersprache Structured Text | ||
| + | * Definition nach IEC-61131-3 | ||
| + | * Formalisierung als Kontrollflussgraph | ||
| + | * Statische Analyse | ||
| + | * Datenflussanalysen | ||
| + | * Ordnungstheoretische Grundlagen (Complete Lattice) | ||
| + | * Live Variables Analysis | ||
| + | * Reaching Definitions Analysis | ||
| + | * Value Set Analysis | ||
| + | * Program Dependency Graphs | ||
| + | * Slicing | ||
| + | * Policy Iteration | ||
| + | * Abstract Interpretation | ||
| + | * Galois-Verbindungen | ||
| + | * Structural Operational Semantics | ||
| + | * CEGAR-Variant for PLC State Space exploration | ||
| + | * Relational Domains | ||
| + | * Specification and Model Checking | ||
| + | * CTL | ||
| + | * Specification Automata | ||
| + | * Logical Characterisation and Symbolic Reasoning | ||
| + | * SMT encoding of Structured Text | ||
| + | * Symbolic Execution | ||
| + | * Large Block Encoding | ||
| + | * Bounded Model Checking | ||
| + | * IC3/PDR | ||
| + | |||
| + | === Termine === | ||
| + | |||
| + | Die regelmäßigen Veranstaltungstermine sind ab dem 08.10. immer Montag, von 10:30-12:00 im Hörsaal AH II, und Mittwoch, von 10:30-12:00 im Hörsaal AH II, im Hauptbau des Informatikgebäudes. Weitere Informationen werden im L2P und im ersten Vorlesungstermin veröffentlicht. | ||
| + | |||
| + | === Vorlesungs- und Übungsbetrieb === | ||
| + | |||
| + | Es werden regelmäßig Übungsblätter veröffentlicht und in den Übungen in Zusammenarbeit mit den Studierenden gelöst. Die Übungen finden ebenfalls in den unter ' | ||
| + | |||
| + | === Klausur === | ||
| + | |||
| + | Die erste Klausur findet am 04.02.2019 um 10:30 statt (AH I, AH III, BS I) -- die Nachholklausur am 06.03.2019 um 10:30 (AH II, AH III). | ||
| + | |||
| + | |||
| + | Klausurrelevant sind die Inhalte aller Vorlesungen und Übungen. | ||
| + | |||
| + | === L2P === | ||
| + | |||
| + | Lernraum wird so bald wie möglich bekanntgegeben. | ||
| + | |||
| + | === Kontakt === | ||
| + | |||
| + | * [[: | ||
| + | * [[: | ||