Mieke Massink
Mieke Massink received her master's degree in computer science from the University of Nijmegen, The Netherlands in 1988; she received her Laurea in Computer Science from the University of Pisa in 1995 and her PhD degree in computer science from the University of Nijmegen in 1996. In 1992 she received the "Dr. I.B.M. Frye Stipend" of the University of Nijmegen for the most promising female PhD researcher. She is currently a researcher in the Formal Methods and Tools lab at CNR-ISTI (Institute of Information Science and Technology ``A. Faedo''), a computer science research institute of the National Research Council of Italy (CNR). Prior to this she held positions at the University of Nijmegen, The University of Twente, both in the Netherlands, and in the context of several European projects, the CNR-CNUCE institute, Italy, and the University of York, United Kingdom. She has been lecturing at the University of Pisa from 1996 to 1998 and from 2006 to 2009, at the University of Florence from 2005 to 2017. Currently she is lecturing in the Tuscan PhD program in Smart Computing from 2015; in Feb. 2011 she was Visiting Professor at the MT-Lab, DTU, Copenhagen, DK. She has served as PC member/chair of numerous conferences and workshops. Her research interests include the development and application of formal languages for specification and verification of concurrent, safety critical and software intensive systems including collective adaptive systems which may exhibit emergent behaviour. In particular her interest is in semantic models and scalable verification techniques for process algebras and automata, and their extension with aspects of mobility, time, space e/o probability and human interaction aspects, and temporal and modal logics for the specification and verification of related properties through logic-based model checking.
Mean Field Model Checking of Population Models
The analysis of large swarm robotics systems (SRSs) directly with robots or using detailed physics-based simulations
is very complex and often time consuming. For this reason it is convenient to analyse new ideas first in a more abstract way
based on (simplified) models. These can more easily be adapted and
analysed from various points of view for example
concerning correctness and performance aspects. Once
the models show convincing behaviour, they can inform
the selection of specific tests with real swarms or
more detailed simulation based approaches.
In earlier work the advantage has been shown of the use of a single model description that allows for various kinds of analysis, among which (stochastic) simulation, statistic (simulation based) model checking and mean field analysis. In recent work model checking techniques have been combined with mean field analysis resulting in a mean field model checking approach. This formal analysis approach, when applicable, is orders of magnitude faster than simulation-based approaches, while retaining the advantages of a logic-based verification method separating concerns of property formulation and model specification.
We illustrate the mean field model checking approach and the associated prototype tool FlyFast and discuss its potential and limitations. We also provide a new theoretical result for the analysis of medium size collective systems and some open problems.
