QUANTITATIVE MODEL CHECKING OF SOFTWARE

Formal Approaches to Model-Driven Quality of Service
Energy Aware Networking Principles
Validation of Multiprocessor Multithreaded Architectures
Quantitative Model Checking of Software

Quantitative Model Checking of Software

Computer aided verification has seen remarkable successes in the last decade. Hardware model checking has become an integral part of daily industrial practice, and software verification is gaining more and more momentum. Verification of entire software systems is the next challenge. While compositionality is often considered as the key to mastering large software correctness proofs, it must also be acknowledged that such systems operate under omnipresent stochastic influences (component failures, resource conflicts, signal perturbations, etc.) Therefore, Boolean correctness results are generally not realistic. Instead, model checking of such systems must allow one to quantify the uncertainty with which correctness guarantees do hold. Holger Hermanns and his coworkers have pioneered the area of quantitative model checking, which allows one to check precisely that. In this approach, models to be verified are stochastic processes or stochastic decision processes. Quantitative requirements are formulated in a temporal logic, which allows one to express requirements such as: "The worst case probability to receive no reply within 5 seconds after a request is bounded by 10-5." Efficient model checking algorithms and corresponding data structures have been devised, implemented, and are being applied in various application areas.

 

Recent achievements of the Dependable Systems and Software chair in this context are:


  • Flow faster: Efficient decision algorithms for probabilistic simulation. This is a TACAS 2007 contribution with Lijun Zhang, Fritz Eisenbrand and David N. Jansen. We present efficient algorithms for an important class of problems, that has rich practical applications in stochastic model checking, but also manifold in security. The principal question is, how to decide whether two Markov chains are similar (in a strict or weak sense), or better, whether one can simulate the behaviour of the other. Our algorithms improve the state-of-the-art by a polynomial factor, as large as n10, where n is the size of the model.
  • Probabilistic model checking modulo theories. Probabilistic models are widely used to analyse embedded, networked, and more recently biological systems. Existing numerical analysis techniques are limited to finite-state models and suffer from the state space explosion problem. As a consequence, the user often has to manually abstract the intended model to get a tractable one. This work, which is performed jointly with Lijun Zhang and Björn Wachter, develops a predicate abstraction toolkit for probabilistic model checking. We leverage recent advances in automatic theorem proving to compute tractable finite-state models. To the best of our knowledge, this is the first time that properties of probabilistic infinite-state models have been verified at this level of automation. First experiments and results are very promising.
  • Almost minimal phase-type representations. Phase-type (PH) distributions have been enjoying increasing attention since their introduction. They are used in stochastic modelling in various areas of applications, such as queueing theory, reliability analysis and computer networks. They also arise in dynamic fault tree analysis and stochastic model checking. Owed to recent work by Reza Pulungan, we are in the position to propose a procedure for reducing the size of the state space of any given acyclic phase-type representations. The approach is computationally simple and therefore well-suited as a preprocessing step to reduce the state space size, prior to other state-space based analyses.