A Probabilistic Model Checking Analysis of Vehicular Ad-Hoc Networks This paper describes a formal probabilistic analysis of protocols and applications proposed in VehicularAd-Hoc Networks (VANET). Services using this technology have been studied and must be tested in a realistic way in order to work properly. Therefore, we have proposed a complete modeling structure which includes mobility, communication and signal propagation modules. We have used PRISM, a model checker for probabilistic systems, instead of traditional simulations. It determines exact probabilities and performance bounds,even if the model is non-deterministic. We present an analysis of a Vehicular Warning System involving three automobiles. The case study shows the influence of the initial positions, speed and timeout on communication, indicating that an interval of three seconds to broadcast packages is enough to guarantee 99% of reception’s chance with a good message traffic. Furthermore, this work presents a practical example to future analysis of VANET.