This material is part of the UE6 module taught as part of the M2 mSSB master at University of Evry. The UE6 module is concerned with teaching of formal methods in the context of biological modelling. Specifically in this part of the course we look at application of formal methods for modeling the dynamics of biochemical reactions represented in terms of a stochastic process. We will see how systems of biochemical reactions can be mapped onto continuous time Markov-chain (CTMC) models and how we can take advantage of expressive temporal logic specification languages to analyse their behaviour. We will look at some concrete case-studies by application of the PRISM model checker tool.