Efficient IoT-Based Formal Model for Vehicle-Life Interaction in VANETs Using VDM-SL
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 form...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2022-01-01
|
| Series: | Energies |
| Subjects: | |
| Online Access: | https://www.mdpi.com/1996-1073/15/3/1013 |
| _version_ | 1797488077289029632 |
|---|---|
| author | Sidra Iqbal Nazir Ahmad Zafar Tariq Ali Eman H. Alkhammash |
| author_facet | Sidra Iqbal Nazir Ahmad Zafar Tariq Ali Eman H. Alkhammash |
| author_sort | Sidra Iqbal |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-03-09T23:56:59Z |
| format | Article |
| id | doaj.art-f1eee1644f754f06b15573fd23f7b670 |
| institution | Directory Open Access Journal |
| issn | 1996-1073 |
| language | English |
| last_indexed | 2024-03-09T23:56:59Z |
| publishDate | 2022-01-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Energies |
| spelling | doaj.art-f1eee1644f754f06b15573fd23f7b6702023-11-23T16:23:47ZengMDPI AGEnergies1996-10732022-01-01153101310.3390/en15031013Efficient IoT-Based Formal Model for Vehicle-Life Interaction in VANETs Using VDM-SLSidra Iqbal0Nazir Ahmad Zafar1Tariq Ali2Eman H. Alkhammash3Department of Computer Science, Sahiwal Campus, COMSATS University Islamabad, Sahiwal 57000, PakistanDepartment of Computer Science, Sahiwal Campus, COMSATS University Islamabad, Sahiwal 57000, PakistanDepartment of Computer Science, Sahiwal Campus, COMSATS University Islamabad, Sahiwal 57000, PakistanDepartment of Computer Science, College of Computers and Information Technology, Taif University, P.O. Box 11099, Taif 21944, Saudi ArabiaVANETs 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.https://www.mdpi.com/1996-1073/15/3/1013VANETsIoTfog-based RSUsformal methodsverification and validation |
| spellingShingle | Sidra Iqbal Nazir Ahmad Zafar Tariq Ali Eman H. Alkhammash Efficient IoT-Based Formal Model for Vehicle-Life Interaction in VANETs Using VDM-SL Energies VANETs IoT fog-based RSUs formal methods verification and validation |
| title | Efficient IoT-Based Formal Model for Vehicle-Life Interaction in VANETs Using VDM-SL |
| title_full | Efficient IoT-Based Formal Model for Vehicle-Life Interaction in VANETs Using VDM-SL |
| title_fullStr | Efficient IoT-Based Formal Model for Vehicle-Life Interaction in VANETs Using VDM-SL |
| title_full_unstemmed | Efficient IoT-Based Formal Model for Vehicle-Life Interaction in VANETs Using VDM-SL |
| title_short | Efficient IoT-Based Formal Model for Vehicle-Life Interaction in VANETs Using VDM-SL |
| title_sort | efficient iot based formal model for vehicle life interaction in vanets using vdm sl |
| topic | VANETs IoT fog-based RSUs formal methods verification and validation |
| url | https://www.mdpi.com/1996-1073/15/3/1013 |
| work_keys_str_mv | AT sidraiqbal efficientiotbasedformalmodelforvehiclelifeinteractioninvanetsusingvdmsl AT nazirahmadzafar efficientiotbasedformalmodelforvehiclelifeinteractioninvanetsusingvdmsl AT tariqali efficientiotbasedformalmodelforvehiclelifeinteractioninvanetsusingvdmsl AT emanhalkhammash efficientiotbasedformalmodelforvehiclelifeinteractioninvanetsusingvdmsl |