Automatic verification of stochastic processes: certification of building automation systems

Smart buildings are key to reducing greenhouse gas emissions in the face of the continuous and fast-paced growth of urbanisation. The performance criteria for the optimal operation of such intelligent systems require the coupling of certification goals with the design of both the modelling framework and control algorithms. In the first part of this thesis we demonstrate the use of Fault Maintenance Trees (FMTs): a qualitative description that embeds component degradation, maintenance policies and the relationship between components leading to a failure. We provide semantics to FMTs using continuous-time Markov chains and employ efficient probabilistic model checking to analyse the performance of heating, ventilation and air-conditioning unit, against certification metrics, under different maintenance schemes. The method is also benchmarked against the application of statistical model checking for analysis. The second part introduces the modelling framework of discrete-time Stochastic Hybrid Systems (SHS): probabilistic models suitable for describing the dynamics of variables presenting interleaved and interacting continuous and discrete components. We present algorithms and techniques for performing scalable verification and control synthesis of SHS. The kernel of the methods is a novel abstraction procedure that makes use of interval Markov decision processes. The method embeds the exact abstraction error within the abstraction itself. Consequently reducing the number of states required significantly and allowing us to analyse SHS with more than 10 continuous variables. Furthermore, the applicability of the framework is shown via the construction and analysis of a library of models for building automation systems with different certification goals. Finally, we embed the models and algorithms within StocHy: a new tool aimed at simplifying the analysis of \shs. The tool is written in C++ and allows for simulation, verification and synthesis of stochastic and hybrid systems, in a manner that is accessible to general end-users