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
