Probabilistic Model Checking-Based Survivability Analysis in Vehicle-to-Vehicle Networks

摘要

Probabilistic model checking has been widely applied to quantitative analy-sis of stochastic systems, e.g., analyzing the performance, reliability and survivability of computer and communication systems. In this paper, we extend the application of probabi-listic model checking to the vehicle to vehicle (V2V) networks. We first develop a contin-uous-time Markov chain (CTMC) model for the considered V2V network, after that, the PRISM language is adopted to describe the CTMC model, and continuous-time stochastic logic is used to describe the objective surviv-ability properties. In the analysis, two typical failures are considered, namely the node fail-ure and the link failure, respectively induced by external malicious attacks on a target V2V node, and interrupt in a communication link. Considering these failures, their impacts on the network survivability are demonstrated. It is shown that with increasing failure strength, the network survivability is reduced. On the other hand, the network survivability can be improved with increasing repair rate. The pro-posed probabilistic model checking-based ap-proach can be effectively used in survivability analysis for the V2V networks, moreover, it is anticipated that the approach can be conve-niently extended to other networks.