Computer systems are complex. From the interaction of programs and services in an operating system to web services on computer networks, from autonomic robot control to interaction between smart devices, sensors and humans, modern computer science has to tackle complexity on a large scale, developping techniques to design and verify thise systems. This need becomes more and more stringent as those systems become ubiquitous in our society.
Classically, interacting parallel processes are controlled by abstracting them in a qualitative and non-deterministic setting. Nowadays, however, design and contol require to be based on quantitative measures and probabilistic abstractions.
This is leading to the fusion of modelling, design and analysis techniques of classical formal methods (like process algebras, formal verification of properties expressed in suitable logical formalisms, and qualitative analysis of components) with modelling and analysis techniques typical of applied mathematics and systems theory (dynamical systems, stochastic processes, statistics).
The result of this integration are powerful frameworks for modelling and analyzing systems, by no means confined to the world of computer science and can be straighforwardly applied to other complex systems, like bilogical systems, ecological networks, socio-technical systems (e.g. social networks).
This course aims at providing an introduction to this field, presenting or recalling the main mathematical ingredients, among which process algebras, stochastic processes (mainly Markov chains), simulation, temporal logics, model checking, hybrid automata, complex networks. This will be supported by examples taken from application areas like computer systems, biology, ecology.
Classically, interacting parallel processes are controlled by abstracting them in a qualitative and non-deterministic setting. Nowadays, however, design and contol require to be based on quantitative measures and probabilistic abstractions.
This is leading to the fusion of modelling, design and analysis techniques of classical formal methods (like process algebras, formal verification of properties expressed in suitable logical formalisms, and qualitative analysis of components) with modelling and analysis techniques typical of applied mathematics and systems theory (dynamical systems, stochastic processes, statistics).
The result of this integration are powerful frameworks for modelling and analyzing systems, by no means confined to the world of computer science and can be straighforwardly applied to other complex systems, like bilogical systems, ecological networks, socio-technical systems (e.g. social networks).
This course aims at providing an introduction to this field, presenting or recalling the main mathematical ingredients, among which process algebras, stochastic processes (mainly Markov chains), simulation, temporal logics, model checking, hybrid automata, complex networks. This will be supported by examples taken from application areas like computer systems, biology, ecology.
- Teacher: LUCA BORTOLUSSI