English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Open

One of the applications of vehicular ad-hoc networks is warning messagedissemination among vehicles in dangerous situations to prevent more damage.The only communication mechanism for message dissemination is multi-hopbroadcast; in which, forwarding a received message have to be regulated using ascheme regarding the selection of forwarding nodes. When analyzing theseschemes, simulation-based frameworks fail to provide guaranteed analysisresults due to the high level of concurrency in this application. Therefore,there is a need to use model checking approaches for achieving reliableresults. In this paper, we have developed a framework called VeriVANca, toprovide model checking facilities for the analysis of warning messagedissemination schemes in VANETs. To this end, an actor-based modeling language,Rebeca, is used which is equipped with a variety of model checking engines. Toillustrate the applicability of VeriVANca, modeling and analysis of two warningmessage dissemination schemes are presented. Some scenarios for these schemesare presented to show that concurrent behaviors of the system components maycause uncertainty in both behavior and performance which may not be detected bysimulation-based techniques. Furthermore, the scalability of VeriVANca isexamined by analyzing a middle-sized model.

VeriVANca: An Actor-Based Framework for Formal Verification of Warning Message Dissemination Schemes in VANETs