VeriVANca framework: verification of VANETs by property-based message passing of actors in Rebeca with inheritance

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.