VeriVANca framework: verification of VANETs by property-based message passing of actors in Rebeca with inheritance
- PDF / 1,835,648 Bytes
- 17 Pages / 595.276 x 790.866 pts Page_size
- 52 Downloads / 169 Views
STTT Special Issue: SPIN 2019
VeriVANca framework: verification of VANETs by property-based message passing of actors in Rebeca with inheritance Farnaz Yousefi1 · Ehsan Khamespanah2,3 · Mohammed Gharib4 · Marjan Sirjani3,5 · Ali Movaghar1
© Springer-Verlag GmbH Germany, part of Springer Nature 2020
Abstract Vehicular ad hoc networks have attracted the attention of many researchers during the last years due to the emergence of autonomous vehicles and safety concerns. Most of the frameworks which are proposed for the modeling and analysis VANET applications make use of simulation techniques. Due to the high level of concurrency in these applications, simulation results do not guarantee the correct behavior of the system and more accurate analysis techniques are required. In this paper, we have developed a framework to provide model checking facilities for the analysis of VANET applications. To this end, an actor-based modeling language, Rebeca, is used which is equipped with a variety of model checking engines. We have extended Rebeca with the inheritance mechanism to support model-specific message passing among vehicles, which is crucial for the modeling of VANET applications. To illustrate the applicability of this framework, we modeled and analyzed two warning message dissemination schemes. Reviewing the results of using the model checking technique supports the claim that concurrent behaviors of the system components in VANETs may cause uncertainty which may not be detected by simulation-based techniques. We also observed that considering the interleaving of concurrent executions of the system components affects the performance metrics of it. Keywords Model checking · Warning message dissemination · Vehicular ad hoc networks (VANETs) · Rebeca · Actor model
1 Introduction Safety of the autonomous vehicles is turned into one of the main concerns of future transportation systems. This concern has been attracting the attention of researchers in both academia and industry, during the last years. Using autonomous vehicles in mission-critical applications increases the significance of the problem. Vehicular ad hoc networks (VANETs) are considered as the main communica-
B
Ehsan Khamespanah [email protected]
1
Department of Computer Engineering, Sharif University of Technology, Tehran, Iran
2
School of Electrical and Computer Engineering, University of Tehran, Tehran, Iran
3
School of Computer Science, Reykjavik University, Reykjavik, Iceland
4
School of Computer Science, Institute for Research in Fundamental Science (IPM), Tehran, Iran
5
School of IDT, Mälardalen University, Västersås, Sweden
tion network in such systems where the main responsibility is the warning message dissemination (WMD). To prevent further potential damage, WMD is used for vehicle to vehicle communication in dangerous situations. In this case, vehicles with the knowledge of hazard broadcast warning messages to inform the other vehicles. To increase the number of vehicles receiving the warning message, the receiving nodes have
Data Loading...
