Efficient IoT-Based Formal Model for Vehicle-Life Interaction in VANETs Using VDM-SL

Sidra Iqbal, Nazir Ahmad Zafar, Tariq Ali and Eman H. Alkhammash
Additional contact information
Sidra Iqbal: Department of Computer Science, Sahiwal Campus, COMSATS University Islamabad, Sahiwal 57000, Pakistan
Nazir Ahmad Zafar: Department of Computer Science, Sahiwal Campus, COMSATS University Islamabad, Sahiwal 57000, Pakistan
Tariq Ali: Department of Computer Science, Sahiwal Campus, COMSATS University Islamabad, Sahiwal 57000, Pakistan
Eman H. Alkhammash: Department of Computer Science, College of Computers and Information Technology, Taif University, P.O. Box 11099, Taif 21944, Saudi Arabia

Energies, 2022, vol. 15, issue 3, 1-27

Abstract: VANETs have gained much attention from both industry and academia because of their characteristics, such as dynamic topology. There are various applications of VANETs that are classified on the basis of safety, efficiency, commercial usage, and productive areas. This paper presents an IoT-based formal model for vehicle-life integration enabling RSUs with the help of different approaches. We have developed a model that uses vehicle scenarios in smart transportation systems so that quick data transmission is provided between the source and destination vehicles. Further, fog-based RSUs provide a wide range to communicate with hospitals and emergency vehicles to deal with emergency situations. All the appropriate entities are connected to ensure a consistent traffic flow for the arrival of an emergency vehicle in emergency places. The UML, graph theory, and VDM-SL formal technique are used to represent this system. To model the network and discover appropriate paths for V2V communication, graph theory is applied. The system requirements are designed using a UML diagram. The VDM-SL, an object-oriented model-based formal technique, was utilized for this modeling procedure. This approach assures the safety and accuracy of systems by detecting flaws early in the design process. It also gives an exceptionally important answer to an issue and increases trust in the software’s quality.

Keywords: VANETs; IoT; fog-based RSUs; formal methods; verification and validation (search for similar items in EconPapers)
JEL-codes: Q Q0 Q4 Q40 Q41 Q42 Q43 Q47 Q48 Q49 (search for similar items in EconPapers)
Date: 2022
References: View complete reference list from CitEc
Citations:

Downloads: (external link)
https://www.mdpi.com/1996-1073/15/3/1013/pdf (application/pdf)
https://www.mdpi.com/1996-1073/15/3/1013/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jeners:v:15:y:2022:i:3:p:1013-:d:738128

Access Statistics for this article

Energies is currently edited by Ms. Agatha Cao

More articles in Energies from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().