Istituto di Scienza e Tecnologie dell'Informazione     
Massink M., Ter Beek M. H., Feng C., Hillston J., Tribastone M. Scalability beyond population size and quantitative product family engineering. QUANTICOL: A Quantitative Approach to Management and Design of Collective and Adaptive Behaviours. Deliverable D3.2, 2015.
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.
URL: http://blog.inf.ed.ac.uk/quanticol/files/2015/09/D32Scalability-beyond-population-size-and-quantitative-product.pdf
Subject Collective Adaptive Systems
Software Product Line Engineering
Model checking
Mean field analysis
Ordinary Differential Equations
Variability analysis
Markov chains
Modal logic
Process algebra
B.8.2 Performance Analysis and Design Aids
D.2.4 Software/Program Verification
D.2.13 Reusable Software
F.1.2 Modes of Computation
F.3.1 Specifying and Verifying and Reasoning about Programs
F.3.2 Semantics of Programming Languages
F.4.1 Mathematical Logic
G.1.7 Ordinary Differential Equations

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional