Lectures

Lectures

Lectures Held on a Regular Basis

Please click here to find the lectures that are held on a regular basis. This information can be used to create a study plan. However, this information is tentative, i.e. always check the lectures of the current and next semester to keep the study plan up to date.

Lectures of the Current Semester

Module details on 'Model Checking - Model Checking'

CategoryTheoretical Foundations
TypeLecture
SiteClausthal
LecturerDr. Huhn, Michaela (Clausthal)
Module Exam ID1065
ECTS-Credits6
Weekly Composition3L+1E
Required Hours of Work (presence / self-study)125 (42 / 83)
Semesterperiodically, according to student demand and staff specialisms
Teaching MethodsSlide presentation, lab exercise, group and individual homework
Module DescriptionThis module will give a broad overview over formally founded, model-based verification methods and techniques used for dependable IT systems, software and hardware. Already in early design phases the precise modelling of the system often reveals inconsistencies and incompleteness which saves the enormous costs of late redesign due to critical findings in traditional testing or after commissioning. The lecture introduces state-transition-systems that form a mathematically precise model suitable to capture the behaviour of industrial-size sequential and distributed programs as well as of hardware components. Then specification formalisms for classes of relevant system properties are presented. The focus of the lecture is on the data structures and algorithms used for exhaustively exploring a state-transition system whether it satisfies a specified property, the so-called model checking techniques.
Module OutcomesOn successful completion of this module, the students know the logical and graph-theoretic foundations and practically applicable model checking tools for dependable systems. Also, they have deep understanding of basic and enhanced data structures and algorithms. This enables students to identify and recognize typical application scenarios for formal modelling and verification. They are able to identify the core components of a system and the critical behavioural properties. They are able to formally model the system and specify the requirements using common formal notations. The students are capable of applying model checking techniques and tools as it is highly recommended for dependable systems. Students are aware of the principal limitations of model-based verification as well as of practical restrictions due to complexity issues, because they know about the capabilities and limits of model checking, and the purpose, strength, and weaknesses of the most common algorithms and system representations. Students are also able to propose heuristic techniques and strategies for dealing with common complexity issues in model checking. In addition, the students learn to deal with scientific source material by working with state-of-the art scientific publications which go far beyond typical capabilities of currently available tools.
Recommended Literature- C. Baier & J.-P. Katoen: Principles of Model Checking, MIT Press, ISBN 026202649X - D. Peled: Software Reliability Methods, Springer, ISBN 1441928766 - K. Schneider: Verification of Reactive Systems: Formal Methods and Algorithms, Springer, ISBN 3642055559
PrerequisitesThe module presumes a prior understanding of automata theory and logic as, for example, acquired through an introductory module on theoretical computer science at undergraduate level.
ExamWritten or oral exam, graded (Written (120 min) / Oral (25 min))
CommentsLive transmission to other Universities

Available Course Modes

In the following document you can get an overview about the available course modes that are offered in the ITIS Master's program: Course Modes