University of Konstanz
Chair for Software Engineering
Prof. Dr. Stefan Leue

Course: Non-Functional Model Checking


Course Material

Course Material  



Bachelor and Master students

Subject Area

Informatik der Systeme / Angewandte Informatik

Contents / Syllabus

Non-functional properties in system design refer to quantifiable aspects of the behavior of a computing system. These include real-time bounds, dependability measures or the development of continuous system parameters. In this course we will introduce into the algorithmic foundations of real-time model checking, stochastic model checking and automated hybrid systems verification. Implementation strategies, tools and application case studies will also be presented. During tutorials students will solve problems and also work with the presented state of the art model checking tools. While this course is self-contained, it complements the courses on "Model Checking of Software" and "Logic in Computer and Software Science".


Further literature will be announced during the course.


SWS: 3
ECTS-points: 5