QUANTICOL - Scalability beyond population size and quantitative product family engineering

The main aim set out for Work Package 3 is the development of the theoretical foundations of novel, scalable and spatial formal analysis techniques and the underlying theories to support the design of large scale CAS. During the first year of the project we have developed several innovative analysis techniques that are highly scalable. Some of these are based on mean field approximation techniques, others involve statistical model checking. In both cases, the development of additional model reduction techniques is very important to further improve scalability of analysis, for example to reduce the number of ordinary differential equations (ODEs) that need to be solved or the number of populations that need to be considered. The description of the project's achievements concerning innovative model reduction techniques constitutes one of the two main parts of this deliverable. In particular this first part addresses: the development of suitable behavioural equivalence relations on ODEs to support model reduction and comparison; a method to identify and remove populations that have no significant impact on a measure of interest; and a method based on automatic moment-closure analysis of population CTMCs. The second part addresses the project's achievements concerning the development of suitable extensions of a software product line engineering (SPLE) approach for CAS. In particular, family-based verification of behavioural aspects of CAS has been pursued. In family-based analysis, the system model covers both behaviour that is common to all products of the family as well as variation points used to differentiate among the individual products that can be derived from the family. This way, logical properties can be analysed at the family level using variability knowledge to deduce results for products, rather than having to generate and analyse each single product, which is often very costly and does not scale well. In this context, an SPLE modelling and analysis framework has been further developed and implemented in the Variability Model Checker VMC that provides family-based verification of qualitative state and action based properties in an on-the-fly fashion. Furthermore, an alternative approach is presented to reason about software product lines focussing on behavioural relations. To this aim the Variant Process Algebra VPA has been developed that has a family-based semantics in which variants can be explicitly labelled. Several quantitative extensions of variability analysis have been developed to handle variability in software performance models. Finally, a first proof-of-concept for feature-oriented modular verification has been developed and, for a restricted notion of coherent branching feature bisimulation, a minimisation algorithm has been developed and its correctness has been shown, as briefly discussed in this report.