The design of collective adaptive systems (CAS for short) must be supported by a powerful, well-founded framework that supports formal modelling and quantitative analysis. CAS consist of a large number of spatially distributed heterogeneous entities with decentralised control and varying degrees of complex autonomous behaviour. These entities or agents may be competing for shared resources even when collaborating to reach common goals. Often humans are both agents within such systems and end-users standing outside them. As end-users, they may be completely unaware of the sophisticated underlying technology needed to fulfil critical socio-technical goals such as effective transportation, communication, and work. The pervasive but transparent nature of CAS, together with the importance of the goals that they address, mean that it is imperative that thorough a priori analysis of their design is carried out to investigate all aspects of their behaviour, including quantitative and emergent aspects, before they are put into operation. We want to have high confidence that, once operational, they can adapt to changing requirements autonomously without operational disruption. Unfortunately, the defining characteristics of these systems mean that their (possibly non-linear) behaviour is often highly unpredictable or counter-intuitive. Formal, scalable, quantitative analysis, which provides multiple perspectives on system behaviour while being based on well-established reasoning techniques, is imperative to master such complex systems.
Our main objective is the development of an innovative formal design framework that provides a unique specification language for CAS and a large variety of tool-supported, scalable quantitative analysis and verification techniques. Such a design framework will also enable and facilitate experimentation and discovery of new design patterns for emergent behaviour and control over spatially distributed CAS. The framework will support both agent-based modelling techniques and equation-based techniques starting from system specifications at the individual (micro) level.
The framework will encompass:
- A compositional (process algebraic) specification language, CAS-SCEL1, for the specification of CAS at the individual (micro) level of the quantitative behaviour of its components, capturing non-functional properties such as availability, reliability and performance.
- Simulation-based analysis that supports agent-based modelling of small to medium sized systems.
- Automatic generation of equation-based models from system specifications at the individual level exploiting mean field and fluid flow techniques to provide population (macro) level analysis.
- Integrated verification techniques including successful existing process algebra techniques, in particular statistical model checking, and the development of completely new model-checking techniques that can deal with very large systems exploiting mean field and fluid flow techniques.
- Extended analysis techniques to deal with large scale, space inhomogeneous, systems and with the control and design of emergence at different scales by advances in mean field and equation-based techniques.
- Extensible integrated tool support for verification and analysis techniques based on CAS-SCEL.
- Design and analysis pathways to guide software engineers in the design and analysis of CAS.
The work in the project will be driven by smart city applications which can be expected to be very large scale CAS comprised of heterogeneous entities with spatially inhomogeneous distribution. This demands computationally scalable approaches. Therefore, the focus of the project is more on the extension and exploitation of mean field and fluid flow techniques than on simulation-based approaches. However, the latter will play an important role in the exploration of smaller systems and in the validation of new techniques. To reach this objective, the QUANTICOL project will bring together two distinct research communities. These are Formal Methods (stochastic process algebras and associated verification techniques); and Applied Mathematics (mean field/continuous approximation and control theory). The envisioned work builds on recent independent breakthroughs by two of the project partners. The first is the discovery of precise scaling conditions under which the global behaviour of collective systems can be well approximated by the solution of a set of differential equations obtained from the individual behaviour of system components and their interaction. The second is the insight that such equations can be directly generated from a compositional stochastic process algebraic specification of the individual behaviour of the single entities of the system and their interaction. The combination of these two breakthroughs has enormous potential. On one hand, it allows the specification of CAS at the individual level of its components and on the other hand the resulting differential equations provide a computationally efficient way to analyse systems with heterogeneous groups of thousands or even millions of interacting entities, possibly exhibiting emergent non-linear behaviour. Moreover, if desired, the same specification can also be used for simulation-based analysis such as is commonly applied to conventional agent-based models.
Although process algebra has been one of the most successful ways to specify concurrent system behaviour, until recently it has not been considered for the specification of large-scale systems such as CAS. The reason for this was the difficulty in automatically and efficiently aggregating discrete behaviour to widen the applicability of analysis and verification techniques typical of process algebras to large-scale systems, especially while preserving an individual (micro) level approach to the specification of heterogeneous behaviour described in terms of the single agents. These difficulties are exacerbated when, as in stochastic process algebra, quantified information is incorporated into the models in order to capture their dynamic behaviour. The exploitation of mean-field approaches and the development of statistical simulation techniques to analyse properties of stochastic process algebraic models are two very promising developments that can overcome limitations in scalability and provide powerful novel verification tools for CAS.
Below we summarise the most crucial scientific breakthroughs that, we believe, can only come about by the specific combination of expertise that is brought together in this project:
• A major scientific breakthrough will be a quantitative model-based design and verification framework that provides:
– a formal modelling language, CAS-SCEL, with primitives that enable the modelling of adaptive, emergent and space dependent behaviour of CAS in a bottom-up manner in terms of behaviour ofindividual components, their mutual interaction and their interaction with the environment.”
– a temporal logic-based language for the formulation of performance related properties of CAS at different levels of abstraction (e.g. both at the individual (micro) level and at the global system (macro) level or mixed).
– an extensive set of scalable analysis and verification techniques and methods, combining and extending quantitative techniques from process algebra, performance analysis, simulation, mean-field approaches and other techniques from the field of complex adaptive systems.
– a software environment in which it is possible to model, analyse, verify and compare CAS designs based on various strategies such as trust, stigmergy and gossip and patterns such as gradient field, negotiation, and tag and token based approaches and to study, experiment and discover novel design principles.
Such a framework is an essential first step towards bringing together knowledge about CAS design that is scattered over many different disciplines and that are currently hard to compare and combine because of the ad hoc and experimental, non-systematic way the field of collective adaptive systems engineering is organised.
• Another scientific breakthrough is expected from the extension of the above framework to the analysis of CAS characterised by inhomogeneous spatial distribution of components. Such arrangement of components arise in the context of the smart cities, as exemplified by our case studies.
• The third important breakthrough will be the development of design principles and analysis pathways for the prediction and control of emergent and (self-)adaptive behaviour and the development of support for such principles and pathways in the context of the formal modelling and verification framework mentioned above.
• Finally, our case studies serve a dual purpose: they provide on one hand a connection to real-world problems that will drive the more theoretical research goals of the project and on the other they will serve as applications to validate the design framework that will be developed in the project and lead to breakthroughs in the application domain, such as new control algorithms for smart grids or better provisioning and capacity planning for transportation systems.