Work Package 3

Logic and Scalable Verification combining Micro and Macro Perspectives

An essential part of any design methodology for CAS is the support of scalable modeling and analyses approaches. The aim of this work package is to combine mean field and fluid flow techniques from applied mathematics with techniques from the area of formal methods to develop such scalable analysis techniques. The work package is split into three main tasks:

  1. The first task focuses on Spatial Stochastic Logics and Scalable Verification. This task deals with the development of probabilistic and stochastic logics and novel model-checking techniques that exploit mean-field and fluid flow techniques that can be used to analyse the behaviour of one component, or a limited set of selected components, in the context of an overall CAS.  Special focus is on spatial aspects of such systems. The logic that will be developed builds on existing stochastic logics extended with operators that can address local, global and combined properties including spatial aspects.
  2. The second task focuses on Abstraction Techniques for Scalability Beyond Population Size. In this task abstractions of CAS models will be investigated with techniques that go beyond fluid approximation. One direction is to consider equivalence relations based on ODEs, with the aim of reducing the number of differential equations to be solved and to provide a bridge between fluid semantics and hierarchical modelling of systems-of-systems. Other directions that will be investigated are reduction techniques that exploit the process algebraic nature or the formal semantics of the models such as lumpability and behavioural equivalences.
  3. The third task focuses on Relating Local and Global System Views with Variability Analysis. The aim of this task is to study the relationship (in terms of properties) between local and global views of a system by using established techniques from variability analysis, as applied in fields like product family engineering. This includes 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 variability of single entities in their overall environment also in a quantitative and scalable setting.

Contact: Mieke Massink – CNR