Quantitative Modeling and Verification of VANET
As VANET become more mission- and even safety–critical, the need for guarantees on adaptive behaviours increases dramatically. It is therefore timely to study the application of formal verification to VANET development, in particular to guarantee that a s
- PDF / 373,721 Bytes
- 6 Pages / 439.37 x 666.142 pts Page_size
- 3 Downloads / 200 Views
Quantitative Modeling and Verification of VANET Jing Liu, Xiaoyan Wang, Shufen Liu, Han Lu and Jing Tong
Abstract As VANET become more mission- and even safety–critical, the need for guarantees on adaptive behaviours increases dramatically. It is therefore timely to study the application of formal verification to VANET development, in particular to guarantee that a system demonstrates the correct behavioural adaptations in all circumstances. In recent years, a complementary technique of probabilistic model checking, an automated verification technique for probabilistic models has been developed. In this paper, we focus on the formal quantitative verification of the probabilistic behaviors of VANET which can be expressed quantitatively and require quantitative verification.
Keywords VANET Quantitative modeling Quantitative verification Interval probabilistic timed automata
345.1 Introduction Software is surreptitiously becoming the backbone of modern society, how to assure the correctness and reliability of software system is one of the most important tasks for computer researcher and developer. Automated verification is a J. Liu China State Shipbuilding Corporation, Beijing, China X. Wang (&) S. Liu H. Lu College of Computer Science and Technology, Jilin University, Changchun, China e-mail: [email protected] S. Liu e-mail: [email protected] H. Lu e-mail: [email protected] J. Tong College of Automotive Engineering, Jilin University, Changchun, China
S. Li et al. (eds.), Frontier and Future Development of Information Technology 2743 in Medicine and Education, Lecture Notes in Electrical Engineering 269, DOI: 10.1007/978-94-007-7618-0_345, Springer Science+Business Media Dordrecht 2014
2744
J. Liu et al.
powerful way to uphold it, which is a technique for establishing certain properties, usually expressed in temporal logic, and verify if these properties hold for a system model [1]. When people want to model and analysis complex systems, some factors such as non-determinism of event occurring, time constraint of event occurring and cost of finishing jobs should be considered. These properties are expressed in temporal logic extended with probabilistic and reward operators. Quantitative verification is an analogous technique for establishing quantitative properties of a system model. In recent years, a complementary technique of probabilistic model checking, an automated verification technique for probabilistic models has been developed [2–4]. Vehicular Adhoc Network (VANET) is a promising approach for future intelligent transportation system (ITS) [5]. With the development of VANET, more requirements are raised up according to the properties of VANET, such as its capacity for information system confidentiality (the prevention of unauthorized disclosure), availability (the prevention of unauthorized suppression of data or resources). However, as VANET become more mission- and even safety–critical, the need for hard guarantees on adaptive behaviours increases dramatically. It is therefore timely to
Data Loading...
