Modeling and verifying clustering properties in a vehicular ad hoc network protocol with Event-B

Abstract Vehicular ad hoc network (VANET) routing protocols resort to clustering in order to optimize broadcast traffic flooding. Clustering schemes usually rely on rules which apply to each vehicle in order to reach a targeted organization in a VANET. Most of the literature works which evaluate clu...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Patrick Sondi, Imed Abbassi, Eric Ramat, Emna Chebbi, Mohamed Graiet
Formato:	article
Lenguaje:	EN
Publicado:	Nature Portfolio 2021
Materias:	Medicine R Science Q
Acceso en línea:	https://doaj.org/article/5c0b19e8c76d4e599cc43d32b725c841
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

id	oai:doaj.org-article:5c0b19e8c76d4e599cc43d32b725c841
record_format	dspace
spelling	oai:doaj.org-article:5c0b19e8c76d4e599cc43d32b725c8412021-12-02T19:04:11ZModeling and verifying clustering properties in a vehicular ad hoc network protocol with Event-B10.1038/s41598-021-97063-32045-2322https://doaj.org/article/5c0b19e8c76d4e599cc43d32b725c8412021-09-01T00:00:00Zhttps://doi.org/10.1038/s41598-021-97063-3https://doaj.org/toc/2045-2322Abstract Vehicular ad hoc network (VANET) routing protocols resort to clustering in order to optimize broadcast traffic flooding. Clustering schemes usually rely on rules which apply to each vehicle in order to reach a targeted organization in a VANET. Most of the literature works which evaluate clustering for VANET focus on performance analysis. However, with autonomous vehicles coming to roadways, more rigorous relationships will be required between clustering rules and the resulting organization, so as to anticipate road safety in a better way. We propose a formal description of the properties which are expected in a VANET, while considering the rules of a given clustering scheme. Using Event-B, we first present a description of the VANET, the vehicles movement and the traffic generated by both routing and application messages. Then, based on an Event-B model of a basic routing protocol of the literature, we describe how the specific rules of a clustering scheme can be modeled along with the properties expected in the resulting organization. Finally, we propose a validation process of the model. This paper aims at showing how our proposals have been applied to the Chain-Branch-Leaf scheme, although they can be adapted to any rule-based clustering scheme for VANET.Patrick SondiImed AbbassiEric RamatEmna ChebbiMohamed GraietNature PortfolioarticleMedicineRScienceQENScientific Reports, Vol 11, Iss 1, Pp 1-15 (2021)
institution	DOAJ
collection	DOAJ
language	EN
topic	Medicine R Science Q
spellingShingle	Medicine R Science Q Patrick Sondi Imed Abbassi Eric Ramat Emna Chebbi Mohamed Graiet Modeling and verifying clustering properties in a vehicular ad hoc network protocol with Event-B
description	Abstract Vehicular ad hoc network (VANET) routing protocols resort to clustering in order to optimize broadcast traffic flooding. Clustering schemes usually rely on rules which apply to each vehicle in order to reach a targeted organization in a VANET. Most of the literature works which evaluate clustering for VANET focus on performance analysis. However, with autonomous vehicles coming to roadways, more rigorous relationships will be required between clustering rules and the resulting organization, so as to anticipate road safety in a better way. We propose a formal description of the properties which are expected in a VANET, while considering the rules of a given clustering scheme. Using Event-B, we first present a description of the VANET, the vehicles movement and the traffic generated by both routing and application messages. Then, based on an Event-B model of a basic routing protocol of the literature, we describe how the specific rules of a clustering scheme can be modeled along with the properties expected in the resulting organization. Finally, we propose a validation process of the model. This paper aims at showing how our proposals have been applied to the Chain-Branch-Leaf scheme, although they can be adapted to any rule-based clustering scheme for VANET.
format	article
author	Patrick Sondi Imed Abbassi Eric Ramat Emna Chebbi Mohamed Graiet
author_facet	Patrick Sondi Imed Abbassi Eric Ramat Emna Chebbi Mohamed Graiet
author_sort	Patrick Sondi
title	Modeling and verifying clustering properties in a vehicular ad hoc network protocol with Event-B
title_short	Modeling and verifying clustering properties in a vehicular ad hoc network protocol with Event-B
title_full	Modeling and verifying clustering properties in a vehicular ad hoc network protocol with Event-B
title_fullStr	Modeling and verifying clustering properties in a vehicular ad hoc network protocol with Event-B
title_full_unstemmed	Modeling and verifying clustering properties in a vehicular ad hoc network protocol with Event-B
title_sort	modeling and verifying clustering properties in a vehicular ad hoc network protocol with event-b
publisher	Nature Portfolio
publishDate	2021
url	https://doaj.org/article/5c0b19e8c76d4e599cc43d32b725c841
work_keys_str_mv	AT patricksondi modelingandverifyingclusteringpropertiesinavehicularadhocnetworkprotocolwitheventb AT imedabbassi modelingandverifyingclusteringpropertiesinavehicularadhocnetworkprotocolwitheventb AT ericramat modelingandverifyingclusteringpropertiesinavehicularadhocnetworkprotocolwitheventb AT emnachebbi modelingandverifyingclusteringpropertiesinavehicularadhocnetworkprotocolwitheventb AT mohamedgraiet modelingandverifyingclusteringpropertiesinavehicularadhocnetworkprotocolwitheventb
_version_	1718377212148711424

Modeling and verifying clustering properties in a vehicular ad hoc network protocol with Event-B

Ejemplares similares