Paper Info
Title
A Probabilistic Model Checking Analysis of Vehicular Ad-Hoc Networks
Abstract
This paper describes a formal probabilistic analysis of protocols and applications proposed in Vehicular Ad-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.
Year
DOI
Venue
2015
10.1109/VTCSpring.2015.7145641
2015 IEEE 81st Vehicular Technology Conference (VTC Spring)
Keywords
Field
DocType
probabilistic model checking analysis,vehicular ad-hoc networks,probabilistic analysis,protocols,VANET,signal propagation modules,PRISM,model checker,probabilistic systems,vehicular warning system,automobiles
Warning system,Broadcasting,Model checking,Computer science,Computer network,Probabilistic analysis of algorithms,Timeout,Probabilistic logic,Wireless ad hoc network,Vehicular ad hoc network,Distributed computing
Conference
ISSN
Citations 
PageRank 
1550-2252
0
0.34
References 
Authors
7
4
Name
Order
Citations
PageRank
Bruno Ferreira100.34
Fernando A. F. Braz242.83
Antonio Loureiro32406197.77
Sérgio Vale Aguiar Campos41344141.08