QUANTITATIVE MODEL CHECKING OF SOFTWARE 


Formal Approaches to ModelDriven 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:


Dependable Systems & Software Group  Department of Computer Science  Universität des Saarlandes 