Formal modelling and scalable analysis of massively parallel systems

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.