The course will introduce the use of formal methods for specifying and verifying qualitative and quantitative properties of complex systems.
First, in the course powerful and well established tools, like Process Algebras and Modal Logics, will be considered.
Process algebras will be used for specifying the behaviour of systems while modal and temporal logics will be considered for the specification of properties. Finally, model-checking techniques will be considered for supporting the verifi
J. Rutten, M. Kwiatkowska, G. Norman, D. Parker
Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems
American Mathematical Society, 2004
Christel Baier and Joost-Pieter Katoen
Principles Of Model Checking
MIT Press, 2008
Learning Objectives
This course aims at introducing students to the main specification and verification techniques based on formal methods. In the course will be presented methods and techniques that support specification and verification of qualitative and quantitative properties of complex systems. The student will also be used specific automatic tools, like PRISM, to perform analysis of different case studies..
Prerequisites
Foundations of logic. Programming principles. Principles of probability.
Teaching Methods
Lectures
Type of Assessment
Oral exam and project
Course program
Process algebras. Linear modal logics: LTL. Model-checking LTL. Branching modal logics: CTL and mu-calculus. Model-checking of CTL: an algorithm global and local algorithm. Model-checking mu-calculus.
Quantitative properties of systems. Discrete-time stochastic systems: DTMC, PCTL, model-checking algorithms. Continuous-time stochastic systems: CTMC, CSL, model-checking algorithms. Advanced techniques for model-checking quantity.