VeriVANca：一个基于 Actor 的 VANETs 警告消息分发方案形式化验证框架
网络与互联网体系结构
2019-05-06 v1
摘要
车载自组织网络的应用之一是在危险情况下在车辆之间分发警告消息以防止更多损害。消息分发的唯一通信机制是多跳广播；其中，接收消息的转发必须使用关于转发节点选择的方案进行调节。在分析这些方案时，由于该应用中的高并发水平，基于仿真的框架无法提供有保证的分析结果。因此，需要使用模型检验方法来获得可靠的结果。在本文中，我们开发了一个名为 VeriVANca 的框架，为 VANETs 中的警告消息分发方案分析提供模型检验工具。为此，使用了一种基于 Actor 的建模语言 Rebeca，该语言配备了多种模型检验引擎。为了说明 VeriVANca 的适用性，展示了对两种警告消息分发方案的建模和分析。展示了这些方案的一些场景，以表明系统组件的并发行为可能导致行为和性能上的不确定性，而这些不确定性可能无法被基于仿真的技术检测到。此外，通过分析中等规模的模型检验了 VeriVANca 的可扩展性。
引用
@article{arxiv.1905.01137,
title = {VeriVANca: An Actor-Based Framework for Formal Verification of Warning Message Dissemination Schemes in VANETs},
author = {Farnaz Yousefi and Ehsan Khamespanah and Mohammed Gharib and Marjan Sirjani and Ali Movaghar},
journal= {arXiv preprint arXiv:1905.01137},
year = {2019}
}