Course teached as: B018971 - METODI FORMALI PER LA VERIFICA DI SISTEMI Second Cycle Degree in COMPUTER SCIENCE
Teaching Language
Italian
Course Content
Formal methods techniques for the analysis of complex systems will be introduced in the course. First, Process Algebras will be used as tool for modelling system behaviour. Hence, modal and temporal logics will be used to specify qualitative and quantitative properties of modelled systems. Finally, model-checking algorithms will be introduced to check if the considered models satisfy or not the requirements.
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.