Formale Verifikation

NUMMER: n.n.
KÜRZEL: ForVer
DOZENT: Prof. Dr. Thomas Zeume
FAKULTÄT: Fakultät für Elektrotechnik und Informationstechnik
SPRACHE: Englisch
SWS: 4 SWS
CREDITS: 5 CP
WORKLOAD: 150 h
ANGEBOTEN IM: jedes Wintersemester

INFOS

Formal Verifikation – Vorlesung (2 SWS)
Formal Verification – Übung (2 SWS)


PRÜFUNGUNGSFORM

Schriftliche Modulabschlussprüfung über 120 Minuten


LERNFORM

Hörsaalvorlesung mit Medienunterstützung, praktische Übungen am Rechner, zusätzlich Selbststudium durch praktische Projektaufgaben


LERNZIELE

Nach dem erfolgreichen Abschluss des Moduls

- beherrschen die Studierenden die Grundlagen der formalen Verifikation
- verstehen die Studierenden das Konzept der Abstraktion von Daten und Transitionen
- verfügen die Studierenden über Werkzeuge zur Verifikation von Software
- kennen die Studierenden die Model-Checking Verfahren und können sie in praktische Algorithmen umsetzen
- sind die Studierenden in der Lage, die verschiedenen Techniken der formalen Spezifikation und Verifikation von Software zu verstehen und praktisch anzuwenden
- sind sich der Studierenden über die praktischen Relevanz der formalen Verifikation von Software bewusst


INHALT

Es ist eine große Herausforderung an die Informatik, automatische Methoden zur Analyse und Verifikation von Verhaltenseigenschaften für Software-Systeme zu entwickeln. Diese Methoden für die formale Verifikation und Spezifikation von Software ergänzen die traditionelle Softwareentwicklungsmethoden und ersetzen sie sogar teilweise. Die Verfahren, dessen Grundlagen auf Logik und Deduktion basieren, müssen in der Praxis auf die jeweiligen Anwendungen und deren Eigenschaften abgestimmt sein, und zwar sowohl die zur Spezifikation verwendeten Sprachen als auch zur Verifikation verwendeten Kalküle.
Die Vorlesung gibt einen Einblick in das Thema Formale Verifikation und gliedert sich wie folgt:

- Einführung in das Thema Formale Verifikation
- Logik (Aussagelogik, temporale Logik)
- Spezifikationsformalismen
- Systemmodellierung und Algorithmen zur Modellprüfung
- Techniken der Automatisierung der Verifikation

Anwendungen (Verifikation funktionaler Eigenschaften imperative und objekt-orientierter Programme, Verifikation nebenläufiger Programme, Verifikation von Echtzeiteigenschaften, Verifikation der Eigenschaften der Datenstrukturen, Programm- und Protokollverifikation)


VORAUSSETZUNGEN

Keine


VORAUSSETZUNGEN CREDITS

Bestandene Modulabschlussprüfung


EMPFOHLENE VORKENNTNISSE

Inhalte des Pflichtmoduls Software Engineering sowie solides Basiswissen aus den Grundlagenmodulen im Bereich Mathematik und Informatik


LITERATUR

1. F. Nielson, H. Nielson, C. Hankin: „Principles of Program Analysis”, Springer Verlag
2. E. M. Clarke, O. Grumberg, D. Peled: “Model Checking”, MIT Press
3. C. Baier and J.-P. Katoen: ”Principles of Model Checking”, MIT Press


Formal Verification

NUMMER: n.n. KÜRZEL: ForVer DOZENT: Prof. Dr. Thomas Zeume FAKULTÄT: Fakultät für Elektrotechnik und Informationstechnik SPRACHE: English SWS: 4 SWS CREDITS: 5 CP WORKLOAD: 150 h ANGEBOTEN IM: each winter semester

INFOS

Formal Verification – Lecture (2 SWS)
Formal Verification – Exercise (2 SWS)


PRÜFUNGUNGSFORM

Written final exam of 120 Minutes


LERNFORM

Lecture with media support, practical exercises on the computer, additional self-study through practical project tasks


LERNZIELE

After successfully completing the module
- the students have mastered the basics of formal verification
- the students understand the concept of abstraction of data and transitions
- the students have tools for verifying software
- the students know the model checking procedures and can implement them in practical algorithms
- the students are able to understand the various techniques of formal specification and verification of software and to apply them practically
- the students are aware of the practical relevance of the formal verification of software


INHALT

It is a great challenge for computer science to develop automatic methods for the analysis and verification of behavioral properties for software systems. These methods for the formal verification and specification of software complement traditional software development methods and even partially replace them. The methods, the fundamentals of which are based on logic and deduction, must in practice be tailored to the respective applications and their properties, both the languages used for specification and the calculi used for verification.
The lecture gives an insight into the topic of formal verification and is structured as follows:
- Introduction to the subject of formal verification
- Logic (propositional logic, temporal logic)
- Specification formalisms
- System modeling and algorithms for model testing
- Verification automation techniques
Applications (verification of functional properties of imperative and object-oriented programs, verification of concurrent programs, verification of real-time properties, verification of the properties of data structures, program and protocol verification)


VORAUSSETZUNGEN

None


VORAUSSETZUNGEN CREDITS

Passed examination


EMPFOHLENE VORKENNTNISSE

Contents of the mandatory course “software engineering” as well as solid basic knowledge from the basic modules in the field of mathematics and computer science


LITERATUR

1. F. Nielson, H. Nielson, C. Hankin: „Principles of Program Analysis”, Springer Verlag
2. E. M. Clarke, O. Grumberg, D. Peled: “Model Checking”, MIT Press
3. C. Baier and J.-P. Katoen: ”Principles of Model Checking”, MIT Press