Probabilistic Model Checking Techniques for the Verification and Synthesis of Software Systems

Probabilistic model checking is a mathematically based technique widely used to verify whether systems with stochastic behaviour satisfy their nonfunctional requirements, and to synthesise new system designs that comply with such requirements. Nevertheless, the technique has a number of limitations. First, the validity of the verification depends on the accuracy of the models being verified—with invalid verification results causing wrong software engineering decisions. Second, the variant of the technique used to perform verification under parametric uncertainty is computationally very expensive. Finally, the synthesis of stochastic models (corresponding to desirable system designs/configurations) is typically only possible for simple requirement combinations, and for discrete-time models. This thesis provides solutions to these limitations. First, we introduce a method for the efficient and accurate verification of nonfunctional requirements under parametric uncertainty. This method collects additional data about the parameters of the verified model by unit-testing specific system components over a series of verification iterations. The components tested in each iteration are decided based on the sensitivity of the model to variations in the parameters of different components, and the overheads (time or cost) of unit-testing these components. Second, we extend the applicability of probabilistic model checking under parametric uncertainty to larger models than currently possible by leveraging recent advances from the area of parametric model checking. Third, we propose a new method for synthesising Pareto-optimal Markov decision process (MDP) policies that satisfy complex requirement combinations. These policies correspond to optimal system designs or configurations, and are obtained by translating the MDPs into parametric Markov chains, and using search-based software engineering techniques to synthesise Pareto-optimal parameter values that define optimal policies for the original MDP. Finally, we present an approach for the synthesis of continuous-time Markov decision process (CTMDP) policies—a problem not addressed by existing probabilistic model checkers. This approach generates policies that define software-system configurations or cyber-physical system controllers that meet predefined nonfunctional constraints and achieve optimal trade-offs between multiple optimisation objectives.