You are here

Formal modelling and scalable analysis of massively parallel systems

3 April 2014
San Francesco - Cappella Guinigi
Many natural and engineered systems can be described in terms of interactions between large populations of relatively simple entities. In this talk I will present a modelling language for such systems. It is rooted in the tradition of formal methods developed in concurrency theory, where a model is interpreted as a Markov process to account for the inherent stochasticity of real systems. Unfortunately, this approach leads to the well-known “curse of dimensionality”, whereby the analysis becomes impractical even for models of moderate size. To tackle this problem, I will overview “fluid interpretation”. This is an approximation in terms of a typically compact system of ordinary differential equations, an approach that has proved useful in a wide variety of disciplines such as physics, chemistry, control theory, and ecology. Despite some significant advantages, I will challenge the applicability of fluid analysis to a number of situations of practical interest, for instance when space and mobility are to be explicitly taken into account; or when the system is organised hierarchically, with macro-entities that may contain sub-entities, with arbitrary levels of nesting. I will present recent solutions to these problems, using techniques of model abstraction and state-space reduction of large-scale dynamical systems. I will also show how our approach yields efficient and accurate predictions of as diverse case studies as bike-sharing systems, chemical reaction networks, distributed and multi-threaded software, and communication networks.
Tribastone, Mirco