See News

Start VPV project VERIFIED PROBABILISTIC VERIFICATION

As from 1 January 2021, the VPV project has started.
Probabilistic verification computes measures of interest—such as the probability of reaching an error state, the  expected accumulated reward, or the long-run average throughput—for large Markov chains or Markov decision  processes described in formal modelling languages. Its applications include safety- and performance-critical systems  faced with probabilistic uncertainty—communication networks, electricity grids, data centres, airplane collision  avoidance—but it is also used to e.g. reason about machine-learnt agents. Probabilistic verification faced a crisis  of trust after the discovery that the standard implementation of a core algorithm, value iteration, cannot actually  deliver quantifiably -correct results. With this project, we aim to fully overcome that crisis, and enable probabilistic  verification to again benefit our society—increasingly reliant on critical digital and cyber-physical systems—through  its various applications. We develop new sound and exact probabilistic model checking algorithms to fill several  gaps in their current coverage of probabilistic formalisms and measures of interest, and to gain deeper insights  into what makes these algorithms (supposedly) correct. We then formalise the semantics of the JANI model interchange  language and of several key algorithms, such that they can be input to an interactive theorem proving  system, e.g. Isabelle/HOL. This allows us to create machine-checked correctness proofs. Based on that formalisation,  we automatically derive a correct-by-construction tool guaranteed to be free of implementation bugs, and  tune its performance via correctness-preserving transformations. We finally develop measure-of-interest-preserving  model transformations in order to expand medium-sized models—for which our verified tool can provide knowncorrect  values—into very large benchmarks that challenge even the most hand-optimised unverified probabilistic  verifiers of tomorrow. At the project’s conclusion, we will have restored the trust in probabilistic verification, and set  an example for other formal techniques for critical systems: they must be verified, and they can be verified.

PRINCIPAL INVESTIGATOR:
Dr. Arnd Hartmanns

INVOLVED RESEARCHER:
Bram Kohlen MSc