We present FlyFast, a recently introduced on-the-fly mean field model checker for the verification of time-dependent probabilistic properties of individual objects in the context of large populations. An example of its use is illustrated analysing a push-pull gossip protocol. Such protocols form the basis on top of which many smart collective adaptive systems are built. Typical properties are the replication of a fresh data element throughout a network, the coverage of the network, and the time to convergence.

Public bike-sharing systems are a popular means of sustainable urban mobility, but their successful introduction in a city stands or falls with their specific designs. What kind of bikes and docking stations are needed, how many and where to install them? How to avoid as much as possible that stations are completely empty or full for some period? Hence, a bike-sharing system can be seen both as a highly (re)configurable system and as a collective adaptive system. In this paper, we present two complementary strategies for the evaluation of bike-sharing system designs by means of automated tool support. We use the Clafer toolset to perform multi-objective optimisation of attributed feature models known from software product line engineering and the recently developed mean field model checker FlyFast to assess performance and user satisfaction aspects of variants of large-scale bike-sharing systems. The combined use of these analysis approaches is a preliminary step in the direction of automatic decision support for the initial design of a bike-sharing system as well as its successive adaptations and reconfigurations that considers both qualitative and performance aspects.