Probabilistic model checking is a powerful tool for the analysis of performance, dependability and other quality properties of software during design, verification, maintenance and at runtime.
However, the usefulness of this tool depends on the accuracy of the (stochastic) models being analysed, and on the ability to select effective designs and parameter values from huge numbers of alternative architectures and configurations.
This talk will show how recent advances in stochastic model learning, synthesis and efficient analysis can help address these major challenges, supporting through-life software quality engineering.