A Probabilistic Model Checking Analysis of a Realistic Vehicular Networks Mobility Model

Vehicular Ad-Hoc Networks (VANET) are a special type of network where its nodes are vehicles that move according to specific patterns. This network is based on wireless communication, presenting new challenges, such as how it will be tested in realistic scenarios. Currently, simulations are widely used. However, they have limitations, such as local minima. Another approach is model checking, which has been used in only a few studies, often overlooking mobility and signal propagation issues. This work provides a realistic mobility model using probabilistic model checking to describe an overtake scenario involving three vehicles in a short distance. Our analysis has shown 98% of accident chance in this situation. However, the main result is providing an example to represent the mobility aspect which can be connected with other models such as signal propagation and the network itself. Therefore, VANETs can now be tested using methods closer to the reality.