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
Leistungsnachweis:
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>
ECTS-Kreditpunkte:
6
Weitere Informationen aus Stud.IP zu dieser Veranstaltung
Bahe, B. (2024). Nichtlineare Stabilitätsuntersuchungen in einem leistungselektronisch dominierten elektrischen Energiesystem.
Boehm, E. (2024). Einfluss des Netzäquivalents auf die Stabilität eines Netzes mit netzbildenden und netzfolgenden Umrichtern.
beendete
2024
Helmich, L. M. (2024). Entwicklung und Simulation eines Effektivwertmodells für STATCOM-Anlagen mit neuartigen Regelstrategien für Pendeldämpfungen in PowerFactory.
Rüter, C. (2024). Einfluss der Netzstärke auf die Kleinsignalstabilität netzbildender Umrichter mit virtueller Oszillator-Regelung.
Schultheiß, J. (2024). Impedanzbasierte Stabilitätsanalyse zur Bewertung der Stabilitätsgrenzen von DC- und AC-Netzen.
2023
Chouiter, B. (2023). Dynamic Phasor Modelling and Comparison to Classical EMT Models.
Helmich, L. M. (2023). Entwicklung und Simulation einer Regelstrategie für die Pendeldämpfung durch STATCOM-Geräte.
Kamma, J. (2023). Umrichtermodellierung zur Repräsentation von Interaktionen im Sinne der Converter-Driven Stability.
Mißfeldt, C. (2023). Einfluss von Zeitverzögerungen auf die Converter-Driven Stability.
Rosenau, Y. (2023). Einfluss netzbildender Umrichter-Regelungsstrukturen auf die "Converter-Driven Stability".
2022
Kumar, M. (2022). Modellierung und Vergleich des Frequenzverhaltens dezentraler Anlagen mit netzbildenden Eigenschaften oder beigestellter Schwungmasse.
Lim, I. (2022). Modelling and Integration of a Hydrogen Storage Power Plant in the 10-Machine New-England Power System.
Rieckborn, N. (2022). Modellierung des Umwandlungsprozesses eines Wasserstoffspeicherkraftwerks.