Smart cities are nowadays subject of many innovation projects, as well as on the political agenda of many (local) governments. Often, in the design of smart services, and discussions in this regard, the emphasis is mainly on the importance of data collection and of communications, particularly with respect to the Internet of things. Less attention is instead directed to the necessary interactions between the various parts (humans, things, programs, communications systems, etc..) and to the need of ensuring that such interactions, essential for a smart city, contribute to the production of high-quality services and reliability. It should be emphasized that these are complex systems, where services can be the result of the collective behavior of agents of various kinds; systems with distinct characteristics of adaptability, and where, for example, the quality of service can be the result of emergent behaviors. Therefore, the study and design of these systems must themselves be smart. QUANTICOL (www.quanticol.eu) is a 7FP EU FET-Proactive research project on the Fundamentals of Collective Adaptive Systems (CAS), started in 2013. It aims to develop new techniques for the formal modeling and quantitative analysis for the design and operational management of collective adaptive systems, with particular attention to the needs of the context of smart cities and their ICT infrastructures. The very fact that these systems are highly distributed, and that their adaptive behavior is based on close and continuous feedback from a large number of consumers and producers with decentralized control, makes such systems typical examples of CAS. The pervasive, yet transparent, nature of these systems, together with the importance of the objectives, require the use of appropriate tools capable also of a priori, design time, analysis of the expected such systems, in order to be able to thoroughly investigate all aspects of their behavior, including quantitative and emerging ones. In essence, we want to be able to be sufficiently confident that, once operating, these systems can not only provide good routine services, but are also able to adapt to changing needs, in an autonomous way and without operational disruption.
The long-term vision of QUANTICOL is the development of a conceptual framework based on formal methods, with sound mathematical and logical basis, to support the design and qualitative and quantitative analysis of CAS for smart cities, also accompanied by a software engineering methodology which is appropriate and specialized for these systems. The strategy adopted by the project is that of a multidisciplinary approach. QUANTICOL, in fact, combines two distinct academic research communities: that of Formal Methods of Computer Science, with particular reference to stochastic process algebras, logics and related automated verification techniques; and that of Applied Mathematics, with particular reference to the techniques of mean-field / fluid-flow approximation and control theory. The main case studies that guide the research activities in the context of QUANTICOL are two: the first deals with problems of scalability and capacity planning for smart urban transport systems, with particular reference to bus management systems and bike sharing systems . The second addresses instead the problems of design and modeling of smart grid, in the field of production systems and distribution of electrical energy.
A year after its inception, the project has already demonstrated the feasibility of the approaches that we intend to follow. For example, the basic techniques used in this first phase of the project have been applied to the modeling and analysis of the public transport system in the city of Edinburgh, with a specific focus on the bus network. Using automatically collected vehicle location data, the QUANTICOL project was able to build accurate models of stochastic bus service in Edinburgh. Then, using software tools for analysis formal based on stochastic logics, it was possible to automatically compute measures such as the probability of completing a journey within a given tolerance window for the arrival times and define an optimal timetable really compatible with the data obtained from previous measurements. It should be emphasized that the probability measures are not the result of ad hoc operations but they were obtained through a specification of requirements made using formulas of mathematical logic, favoring, thus, the possibility of rigorous analysis of the same consistency of such requirements and the automation of the evaluation process.
Another application of the preliminary results of the project consists in modeling, using mean-field approximation techniques, the likely behaviors of a bike-sharing system and the combined use of sophisticated techniques of model-checking, developed with major contribution by ISTI, for the analysis of relevant properties of such behavior. In particular, a central question for a bike sharing system is what would be the optimal number of bicycles in the system in relation to the number and capacity of the parking-slots, at a given rate of requests for bike per unit of time and for a given average time of use. Another aspect which is interesting to understand is the potential, positive or negative impact of a strategy of incentives for users and then see whether it can help to achieve a more equitable distribution of the bikes in the stations. Obviously, it is important to understand the possible effects of such a strategy before adopting it on the field.
What is important to highlight is the fact that the approach allows to easily modify the relevant models and repeat the analysis with ease and relatively low computational cost, which makes them particularly useful to give a first (approximate) answer to "what if?" questions.
The EU project QUANTICOL (http://www.quanticol.eu/) is coordinated by Prof. J. Hillston, Director of the Laboratory for Foundations of Computer Science of the School of Informatics at the University of Edinburgh. The other project partners are the Italian National Research Council (CNR), through the laboratory of Formal Methods and Tools of ISTI, the IMT Advanced Studies Lucca, INRIA in Grenoble, and the University of Southampton.