Correctness is a major concern in embedded systems. Model checking can fully automatically prove 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 at the same time."
But what are the limitations of model checking? How are the models generated from a given design? And how do the underlying reasoning algorithms work so effectively in practice despite a computational complexity of NP hardness and beyond?
The lecture will answer these questions. Open source tools will be used to gather a practical experience.
Further information is available in stud.ip (use link above).
The term dependability summarizes the concepts reliability, availability, maintainability, safety, and security. All of these aspects are interdependent and are not directly encompassed by the functional specification for a system. This makes the design of dependable system difficult even though all embedded or cyber physical systems have to comply with certain dependability requirements.
This lecture covers how to analyze and quantize dependability with a focus on reliability and availability. Moreover, design techniques for dependable systems are covered. This includes general concepts like redundancy as well as techniques chosen for specific levels in the system hierarchy, e.g., digital hardware design or dependable software.
Seminar (Bachelor, Master; IIW, CS): Algorithms, Data Structures, and their Efficient Implementation
Language: Deutsch/ English Further information is available in stud.ip.
Seminar (Bachelor, Master; IIW, CS): Data Mining - Grundlagen, Algorithmen und Datenstrukturen
Language: Deutsch/ English Further information is be available in stud.ip.
Project works (Forschungsprojekte) and Bachelor or Master theses
