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>
Kumar, Melvin (2024). Automatische Erstellung von Simulationsmodellen für die Untersuchung der Auswirkung einer Netzaggregation auf die Kurschlusseigenschaften eines Netzes.
completed
2024
Helmich, L. M. (2024). Entwicklung und Simulation eines Effektivwertmodells für STATCOM-Anlagen mit neuartigen Regelstrategien für Pendeldämpfungen in PowerFactory.
2023
Engemann, T. (2023). Nachbildung des Betriebsverhaltens einer Windkraftanlage in einer Laborumgebung.
Helmich, L. M. (2023). Entwicklung und Simulation einer Regelstrategie für die Pendeldämpfung durch STATCOM-Geräte.
Heunda, J. (2023). Dynamische Lastmodellierung zur adaptiven Schutzparametrierung in elektrischen Verteilnetzen.
Hube, P. (2023). Quantitative Bewertung des Mehrwerts einer adaptiven gegenüber einer konventionellen Netzschutzparametrierung.
Hube, P. (2023). Modellierung und Analyse des Kurzschlussverhaltens von Typ 4 umrichtergekoppelten Windkraftanlagen.
Kock am Brink, J. (2023). Vergleich von Spannungsstabilitätskennzahlen und deren Eignung als Resilienzindex.
Stoffregen, J. F. (2023). Implementierung und Simulation eines Testnetzes für die Mehrwertbetrachtung eines adaptiven Netzschutzes.
2022
Hillebrecht, T. (2022). Entwicklung und Implementierung eines Verfahrens zur Online-Detektion von Spannungsin-stabilitäten in gekoppelten Energiesystemen.
Schill, G. (2022). Untersuchung von Störungskaskaden in sektorengekoppelten Energiesystemen mittels einer Resilienzkennzahl.
2021
Ducci, D. (2021). Untersuchung der Bereitstellung von Regelleistung durch virtuelle Kraftwerke in sektorengekoppelten Energiesystemen.
Gomez Anccas, E. D. (2021). Entwicklung einer Methodik zur quantitativen Untersuchung und Bewertung dynamischer Interaktionen in gekoppelten Energiesystemen.
2020
Dressel, M. (2020). Untersuchung von spannungsstabilitätsbedingten Resilienzveränderungen im norddeutschen Energiesystem.
Gomez Anccas, E. D. (2020). Entwicklung eines Testmodells zur Untersuchung dynamischer Interaktionen in gekoppelten Energiesystemen.
Luo, K. (2020). Untersuchung der Auswirkungen des Netzentwicklungsplans 2025 auf die Netztopologie in Norddeutschland.
2019
Bredenberg, H. (2019). Optimierungssystem zur Netzplanung für die Mittelspannungsebene unter Berücksichtigung möglicher Entwicklungsszenarien.
Faili, Z. (2019). Analysis of the Voltage Stability in the Northern German Electrical Grid with Dynamic Simulation.
Häbel, I. (2019). Aggregation von Netzdaten für die numerisch effiziente Simulation gekoppelter Energiesysteme.
Krupp, M. (2019). Entwicklung und Integration eines Simulationsmodells für vermaschte Mehrpunkt-HGÜ-Systeme im Rahmen der Power System Toolbox.
2018
Dressel, M. (2018). Entwicklung und Integration eines Testnetzes zur Nachbildung des elektrischen Energiesystems von Nordeutschland für die Simuation energietechnischer Szenarien.