Wie kann die Korrektheit von Software und Hardware formal ĂŒberprĂŒft werden? Im Model Checking werden Software- und Hardware-Module durch Transitionssysteme formalisiert; gewĂŒnschte Eigenschaften mit Hilfe logischer Formalismen formal beschrieben; und mit Hilfe von Algorithmen automatisiert ĂŒberprĂŒft, ob ein Transitionssystem eine formal spezifizierte Eigenschaft besitzt.
In dieser Veranstaltung werden die theoretischen Grundlagen des Model Checkings vermittelt, mit einem Fokus auf logik-basierten Spezifikationssprachen. Die Spezifikationssprachen LTL und CTL werden eingefĂŒhrt, ihre AusdrucksstĂ€rke untersucht, und die wichtigsten algorithmischen AnsĂ€tze fĂŒr das Model Checking vorgestellt.
In dieser Veranstaltung werden die theoretischen Grundlagen des Model Checkings vermittelt, mit einem Fokus auf logik-basierten Spezifikationssprachen. Die Spezifikationssprachen LTL und CTL werden eingefĂŒhrt, ihre AusdrucksstĂ€rke untersucht, und die wichtigsten algorithmischen AnsĂ€tze fĂŒr das Model Checking vorgestellt.
- Kursleiter/in: Marko Schmellenkamp
- Kursleiter/in: Nils Vortmeier
Semester: WT 2023/24