News | FMT group

Start VPV projectAs 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.
Fri 15 Jan 2021
Read more
Start SAVES project: SCALABLE VERIFICATION OF INDUSTRIAL EMBEDDED CONTROL SYSTEMSAs from 1 January 2021, the SAVES project started.
Embedded systems surround us everywhere in our everyday live. Their functionality spans from simple microcontrollers in a fridge to complex systems with millions of lines of code, for example in cars, airplanes, or smart factories. In such systems, failure often has serious consequences, such as huge financial losses or even loss of lives. Thus, the correctness and reliability of embedded systems are of vital importance. To establish correctness of embedded systems, however, is hard. With trends such as Industry 4.0, the internet of things, and autonomous driving, the complexity of embedded systems is steadily increasing. A prerequisite to ensure the correct functioning of industrial embedded systems under all circumstances is a clear understanding of the models and languages that are used in the development process. Formal methods provide a basis to make the development process systematic, well-defined, and automated. However, for many industrially relevant languages and models, the semantics are only informally defined. Together with the limited scalability of formal design and verification techniques, this makes the formal verification of industrial embedded control systems a difficult challenge, which can not be solved satisfactory with currently available methods and tools. At the same time, we see that in the area of deductive program verification, powerful techniques and tools have been developed to reason about software with unbounded parameters, for example the VerCors tool suite. In this project, we will extend these techniques with concepts to cope with heterogeneity, concurrency, and real-time to make them suitable for industrial embedded systems.

PRINCIPAL INVESTIGATORS:
Fri 15 Jan 2021
Read more

Suggestions