Correctness is a major concern in embedded systems. Model checking can fully automatically proof formal properties about digital hardware or software. Such properties are given in temporal logic, e.g., to prove "No two orthogonal traffic lights will ever be green."
And how do the underlying reasoning algorithms work so effectively in practice despite a computational complexity of NP hardness and beyond?
But what are the limitations of model checking? How are the models generated from a given design? The lecture will answer these questions. Open source tools will be used to gather a practical experience.
Among other topics, the lecture will consider the following topics:
Modelling digital Hardware, Software, and Cyber Physical Systems
Data structures, decision procedures and proof engines
Binary Decision Diagrams
And-Inverter-Graphs
Boolean Satisfiability
Satisfiability Modulo Theories
Specification Languages
CTL
LTL
System Verilog Assertions
Algorithms for
Reachability Analysis
Symbolic CTL Checking
Bounded LTL-Model Checking
Optimizations, e.g., induction, abstraction
Quality assurance
Performance accreditation:
695 - Modellprüfung - Beweiser und Algorithmen<ul><li>695 - Modellprüfung - Beweiser und Algorithmen: mündlich</li></ul><br>m1397 - Modellprüfung - Beweiser und Algorithmen<ul><li>p1309 - Modellprüfung - Beweiser und Algorithmen: mündlich</li><li>vl360 - Verpflichtende Studienleistung Modellprüfung - Beweiser und Algorithmen - Fachtheoretisch-fachpraktische Studienleistung: Fachtheoretisch-fachpraktische Studienleistung</li></ul>
Erxleben, J. (2023). Entwicklung eines Algorithmus zur Identifikation und Klassifizierung relevanter Arbeitspunkte eines elektrischen Systems aus Momentanwert-Datensätzen.
completed
2023
Engemann, T. (2023). Entwicklung einer Methodik zur automatischen Identifizierung, Klassifizierung und Modellierung betriebsrelevanter Arbeitspunkte eines elektrischen Netzes aus Echtzeitmesswerten.
Herzberg, M. (2023). Entwicklung eines echtzeitfähigen Photovoltaiksimulators auf Basis historischer Strahlungsdaten für einen Power Hardware-in-the-Loop Aufbau mit einem PV-Wechselrichter.
Heunda, J.E.W. (2023). Entwicklung, Optimierung und Vergleich von Methoden zur Erzeugung passiver Ersatzschaltbilder aus Messwerten einer Impedanzspektroskopie.
2022
Becker, H. C. (2022). Entwicklung, Implementierung und Verifizierung einer Schnittstellensynchronisation für die Kopplung von in Echtzeit simulierten Anlagen und Komponenten an einen PHiL Laboraufbau.
Hinzke, M. (2022). Untersuchung der Stabilität eines Power Hardware-in-the-Loop Teststandes unter der Verwendung eines Synchrongenerators als Schnittstelle zwischen Simulation und Hardware.
Landenfeld, Jakob (2022). Implementierung und Validierung einer Methode zur Stabilisierung von Power Hardware-in-the-Loop Simulationen mittels einer online-Impedanzmessung auf einem FPGA.
Landenfeld, Jakob (2022). Bestimmung der Stabilitätskriterien eines DC Power Hardware-in-the-Loop Aufbaus zur Untersuchung von Rippelstrom in Gleichstromsystemen.
Müller, E. (2022). Evaluation of different modelling approaches for battery aging to predict capacity fade for optimization of battery operation.
von Krosigk, J. (2022). Analyse und Bewertung einer Einsatzoptimierung für erneuerbare Energieanlagen in Kombination mit Batteriespeichersystemen im Multi-Use Betrieb.
2021
Erxleben, J. (2021). Untersuchung der Performance eines Pools aus Erneuerbaren Energien für die Erbringung von frequenzstützenden Maßnahmen.
von Krosigk, J. (2021). Untersuchung eines neuartigen Ansatzes zur kurz- und mittelfristigen Vorhersage der Netzfrequenz unter der Verwendung künstlicher neuronaler Netze.