VANET信息广播模型定量验证方法

吉林大学学报(理学版)

VANET信息广播模型定量验证方法

王晓天¹, 赵莹莹², 韩啸²

1. 大连东软信息学院计算机科学与技术系, 辽宁大连 116023；2. 吉林大学学报编辑部, 长春 130012

收稿日期:2016-09-23 出版日期:2017-09-26 发布日期:2017-09-26
通讯作者: 韩啸 E-mail:hanxiao@jlu.edu.cn

Quantitative Verification Method for InformationBroadcasting Model in VANET

WANG Xiaotian¹, ZHAO Yingying², HAN Xiao²

1. Department of Computer Science and Technology, Dalian Neusoft University of Information, Dalian 116023, Liaoning Province, China； 2. Editorial Department of Journal of Jilin University, Changchun 130012, China

Received:2016-09-23 Online:2017-09-26 Published:2017-09-26
Contact: HAN Xiao E-mail:hanxiao@jlu.edu.cn

摘要/Abstract

摘要： 针对车用自组网络(VANET)中信息的发送与接收具有随机性和不确定性, 且VAENT节点具有高速移动、拓扑变化快的特点, 提出一种基于模型检测的定量验证方法. 采用区间概率实时自动机(IPTA)模型表示VANET中的节点, 使用区间概率表示自动机状态转换的概率, 以提高VANET广播协议信息传递的可靠性, 并对VANET中信息广播发送与接收的成功概率进行验证, 证明该方法的可行性.

关键词: 定量建模与验证, 区间概率实时自动机, 区间概率分布, 车用自主网络(VANET)

Abstract: Aiming at the characteristics in vehicular ad hoc networks (VANET) such as randomness and uncertainty of sending and receiving information, high speed movement of VAENT node and fast topology change, we proposed a quantitative verification method based on model detection. In order to improve the reliability of VANET broadcast protocol information transmission, the IPTA model of interval probabilistic real\|time automata was used to represent the nodes in the VANET, and using the interval probability to represent the probability of automatic state transition. We verified the successful probability of sending and receiving broadcast information in VANET, and proved the feasibility of the method.

Key words: interval probabilistic real-time automata, quantitative modeling and verification, interval probabilistic distribution, vehicular ad hoc networks (VANET)

中图分类号:

TP311

王晓天, 赵莹莹, 韩啸. VANET信息广播模型定量验证方法[J]. 吉林大学学报(理学版), 2017, 55(05): 1255-1260.

WANG Xiaotian, ZHAO Yingying, HAN Xiao. Quantitative Verification Method for InformationBroadcasting Model in VANET[J]. Journal of Jilin University Science Edition, 2017, 55(05): 1255-1260.

[1]	杨光, 贾焱鑫, 陈翔, 许舒源. 基于深度学习的Stack Overflow问题帖分类方法[J]. 吉林大学学报(理学版), 2021, 59(4): 922-928.
[2]	李芳, 曲豫宾, 陈翔, 李龙, 杨帆. 一种基于类不平衡学习的情感分析方法[J]. 吉林大学学报(理学版), 2021, 59(4): 929-935.
[3]	曲豫宾, 陈翔, 李龙. 可缓解类重叠问题的跨版本软件缺陷预测方法[J]. 吉林大学学报(理学版), 2021, 59(2): 372-378.
[4]	何锴琦, 马宇骁, 张炎, 刘华虓. 一种基于数据的GitHub项目个性化混合推荐方法[J]. 吉林大学学报(理学版), 2020, 58(6): 1399-1406.
[5]	胡黄水, 赵思远, 刘清雪, 王出航, 王婷婷. 基于动量因子优化学习率的BP神经网络PID参数整定算法[J]. 吉林大学学报(理学版), 2020, 58(6): 1415-1420.
[6]	穆翔宇, 范钰, 李苏吉, 张鹏, 刘磊. 一种基于梯度下降算法的蜕变关系生成方法[J]. 吉林大学学报(理学版), 2020, 58(6): 1429-1435.
[7]	王壹铭, 初剑峰, 王永军, 陈彦东. 基于有向无环图的高效区块链共识算法[J]. 吉林大学学报(理学版), 2020, 58(5): 1167-1172.
[8]	骆焦煌. 基于卷积神经网络的粗粒度数据分布式算法[J]. 吉林大学学报(理学版), 2020, 58(4): 906-912.
[9]	吴春琼. 面向大规模数据的特征趋势推理算法[J]. 吉林大学学报(理学版), 2020, 58(2): 364-370.
[10]	楚玺, 周志祥, 邓国军, 邵帅. 模糊图像的不连续边缘智能检测改进算法[J]. 吉林大学学报(理学版), 2019, 57(04): 875-881.
[11]	刘良凤, 刘三阳. 基于权重差异度的动态模糊聚类算法[J]. 吉林大学学报(理学版), 2019, 57(3): 574-582.
[12]	魏晓辉, 许国威, 王兴旺, 徐海啸. 基于节点相似性和链接次数组合时间序列的链接预测[J]. 吉林大学学报(理学版), 2019, 57(3): 583-590.
[13]	刘久彪. 空间数据库反向最近邻聚类方法[J]. 吉林大学学报(理学版), 2019, 57(2): 387-392.
[14]	张世铮. 基于位移Hermite分裂的图像恢复算法[J]. 吉林大学学报(理学版), 2019, 57(1): 97-104.
[15]	王晓天, 边思宇. 基于遗传算法和神经网络的PID参数自整定[J]. 吉林大学学报(理学版), 2018, 56(4): 953-958.