Nowadays so much new and complex software is being developed that there are not enough specialists to properly test all this software. In this project we therefore develop algorithms for automatic software testing. We are inspired by how people find mistakes. People often learn how a new device (for example, a camera) works by playing with it: they press buttons and see what happens. In this way they playfully discover design errors, for example that a user interface is incorrect. Our algorithms learn how a device works by testing it, and are constantly alert to software bugs.

No more system malfunctions? The ZORRO project is working on diagnostic methods for high-tech systems, such as MRI scanners and printers. By continuously monitoring their behaviour with suitable sensors, algorithms from AI can detect anomalous patterns and relate these to their root causes. Suitable measures, such as replacements or repairs, can then prevent failures. We aim at breakthroughs in complexity with ZORRO: not diagnostics for simple components, but for entire systems; efficient monitoring systems that combine different sensor types; automation of diagnostic processes by capturing domain knowledge in diagnostic models and integrate these into the engineering process for high-tech systems.

Can one improve the reliability of the (Dutch) railroads, and reduce the number of disruptions? We think we can, by deploying advanced data analytic techniques. Key idea is to develop novel techniques to learn the failure behavior of railroad elements with machine learning techniques, and get more information about the causing factors. Using this information, we can repair or replace a railroad element just before it fails, thereby reducing the railroad’s planned and unplanned downtime. Since the success of big data analytics crucially relies on an effective combination with domain knowledge, we integrate machine learning with existing and novel algorithms for fault tree analysis, a prominent technique in reliability engineering to represent the propagation of failure through a system. We will closely collaborate with ProRail, the Dutch railroad asset manager, and NS/NedTrain, the rolling stock maintenance company, and analyze four urgent systems: grinding of rail, the SprinterLightTrain, train-wheel contact, and train-infra systems.

Almost every software system has bugs, and they regularly lead to catastrophic consequences, such as patients dying, fortunes of money being lost, and hackers invading into systems, stealing confident data and extorting ransoms. The software that runs on modern parallel computers is prone to concurrency bugs, which are easily made but hard to find by traditional testing methods. This project researches methods and tools to develop provably correct parallel software. The proofs themselves are checked by a small and well-tested piece of software, such that it is very unlikely to erroneously accept incorrect proofs.

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 epsilon-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 known-correct values - into very large benchmarks that challenge even the most hand-optimised unverified probabilistic verifiers of tomorrow. At the projects 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.