by Maurice ter Beek, Luca Bortolussi, Vincenzo Ciancia, Stefania Gnesi, Jane Hillston, Diego Latella and Mieke Massink
It’s smart to be fair. Researchers from the Formal Methods and Tools group of ISTI-CNR are working on scalable analysis techniques to support smart applications for the efficient and equitable sharing of resources in the cities of our future. The research is being carried out under the European FET-Proactive project, QUANTICOL.
The Smart City concept is on the research agenda of many European Union (EU) and other international institutions and think-tanks. As urban populations grow, innovative information and communication technology (ICT) initiatives are seen by many as one of the key factors that will allow modern cities to reach or maintain a good and sustainable quality of life for their inhabitants, allowing for the timely and equitable distribution of resources.
These ICT-based systems are based on decentralised and distributed designs, comprised of many autonomous and interacting entities, known as collective adaptive systems (CAS). CAS are required to adapt their services seamlessly to the changing needs of their users, who also form an integral part of the system. They typically consist of a large number of spatially distributed, heterogeneous entities with decentralised control and varying degrees of complex autonomous behaviour. This requires the development of novel scalable analysis techniques to investigate their dynamic behaviour and support the design and operational management of a wide range of such systems. In the QUANTICOL project [1], three principal case studies drive the development of a design and analysis framework for CAS: two smart urban transportation systems (smart bus systems and bike-sharing schemes) and smart grid applications. We present some of the QUANTICOL research performed at ISTI-CNR.
In the first year of the project, we developed several scalable analysis techniques that exploit mean field and fluid flow techniques, in combination with logic-based model-checking, to support the investigation and prediction of dynamic resource usage. Mean field techniques were originally developed in the field of statistical physics to cope with the analysis of very large scale systems composed of interacting objects such as molecules in a gas. The possibly non-linear behaviour of such systems is conveniently modelled by a deterministic approximation, i.e., the limit for an infinite number of agents, given as the solution of a set of differential equations (in the continuous case) or difference equations (in the discrete case). Their combined application with model-checking techniques provides a way to verify properties of individual entities in the context of a large system on which they depend, but also properties of the global system or combined local and global properties. An example is the study of the potential effects of user-incentives on maintaining a satisfactory distribution of bikes and empty parking slots over time. The extension of these techniques to address spatial aspects, including spatial model-checking, is a major objective of the project [2].
A further objective of QUANTICOL is to study the relationships between (representations of) small populations and a compact (family) representation of a large population ‘built’ from these smaller populations, by indicating the commonalities and variabilities of single entities in their overall environment. As an initial step in this direction, we performed variability analyses on a bike-sharing product line, considering its behaviour to exhibit variability, not only in the kind of features involved but also in the timing and probability characteristics of these features.
In this context, ISTI-CNR initiated a collaboration with “PisaMo S.p.A. azienda per la mobilità pisana”, an in-house public mobility company in the Municipality of Pisa, that had recently introduced a public bike-sharing system (CicloPi) in Pisa. This led to an initial feature model of a family of bike-sharing systems, annotated with attributes and global quantitative constraints aiming to minimize the total cost of a chosen configuration while simultaneously aiming to maximize customer satisfaction and capacity (of docking stations).
We have studied the specification and analysis of the possible behaviour of a family of bike-sharing systems in terms of the capacity of their docking stations in a value-passing modal process algebra, considering a dynamic redistribution scheme as an optional feature. Future work includes studying a further parametric extension of the value-passing modelling and verification environment as well as the addition of a quantitative dimension to the behavioural model.
QUANTICOL will run until March 2017 and is coordinated by Jane Hillston from the University of Edinburgh (UK). Other partners are EPFL (Switzerland), IMT Lucca (Italy), University of Southampton (UK), LMU (Germany), INRIA (France) and ISTI-CNR (Italy). We thank Marco Bertini from PisaMo S.p.A. for generously sharing his knowledge on bike-sharing systems with us.
Links:
QUANTICOL: http://www.quanticol.eu/
PisaMo: http://www.pisamo.it
References:
[1] L. Bortolussi et al.: “A Quantitative Approach to the Design and Analysis of Collective Adaptive Systems, FoCAS’13, Taormina, Sicily, Italy, 2013
[2] J. Hillston: “Challenges for Quantitative Analysis of Collective Adaptive Systems”, TGC 2013, Buenos Aires, 2013, Springer LNCS, Vol. 8358, pp.14-21, 2014, DOI: 10.1007/978-3-319-05119-2_1.
Please contact:
Mieke Massink, ISTI-CNR, Italy
E-mail:
