Methods of Analysis for Verification of Quantitative properties – MAVEriQ

The variety of challenges laid down by software-driven systems (in particular cyber-physical systems) call all the time for new techniques for assessing their performance, safety and security. Beyond the Boolean question whether a given system satisfies these properties, one would rather ask how much it does so.

Thus, researchers have introduced different quantitative properties: probability of violating the specification, value of simulation games, quantitative semantics of specification logics, robustness measures, entropy as information measure or entropy rate of the set of bad behaviors. For computing their values, usual model-checking approaches were augmented with various quantitative technicalities: linear programming, game-theoretic approaches, differential and integral equations etc.

This diversity causes several issues, making quantitative verification extremely challenging. We can state the difficulty for choosing the most relevant technique among already existing ones (because of non consistent presentation styles and choices of terminology) and the tediousness of developing appropriate variants for each criterion which we want to evaluate.

We believe that, because common patterns are used in many cases, for quantitative verification of timed, hybrid, and/or stochastic systems, the above issues can be strongly mitigated by developing unified frameworks. For instance, we noticed similar are the work-flows for handling probability distributions in Markov Chains, language volumes in timed automata (TA) and probability distributions of runs in stochastic timed automata. First, state space, transitions and behaviors are endowed with a measure, then a measure transforming transfer operator is defined, and finally several properties of the model can be determined as spectral properties of the operator (stationary distributions, volume growth rate/entropy, ... ). In the above example, the common pattern is clear. We believe that by allowing some variations, many more instances could be unified.

The notion of transfer operator (and associated measure) is central in the methods we want to promote (its spectrum yields many pieces of information about algorithms based on iterations of the operator: convergence, speed of convergence, fixed point, ... ). As such, it is the topic of our first work package.

Questions of the form ``How many behaviors are there?'' or ``How much does it cost?'' can easily be formalized in terms of iterations of an operator. Unfortunately, answering the question may have a high algorithmic complexity or the question may be undecidable. For this reason, the second work package focuses on abstraction and approximation techniques for efficiently answering such questions. A prototype tool will be provided and tested on a case study (robust control of cyber-physical systems).

Other questions (robustness questions) have the form ``How far from reaching a bad state are the behaviors of the system?'' or ``How far can we perturb a model or its execution while still avoiding bad states?''. Such statements depend on the notion of distance, of which several versions can be considered, with different properties. Comparative study of distances, their links with the operator method and their application to robustness problems is the topic our third work package.

Last, when the complexity of the model is too high or when there is no complete model of the system to begin with (black box) (often true for cyber-physical systems), validation requires the use of simulation technique, for which different sampling methods exist. In the last work package, we consider exhaustive sampling up to distance $\varepsilon$ (linked with study of distances) and uniform random sampling (linked to study on measures and operators). These techniques will also be implemented in a tool and tested on CPS case studies from the ARCH Workshop (contributed by industrial actors).