Vérification de propriétés d'une méthode de clustering pour réseaux de véhicules par la simulation à événements discrets

La conception des protocoles pour les réseaux de communication repose sur des modèles fonctionnels élaborés selon les besoins du système. Dans les systèmes de transport intelligents, les fonctionnalités étudiées incluent l'auto-organisation, le routage, la fiabilité, la qualité de service et la sécurité. Les évaluations par simulation sur les protocoles dédiés aux ITS (Systèmes de Transport Intelligents) se focalisent sur les performances dans des scénarios spécifiques. Or, l'évolution des transports vers les véhicules autonomes nécessite des protocoles robustes aux propriétés garanties. Les approches formelles fournissent la preuve automatique de certaines propriétés, mais d'autres nécessitent une preuve interactive impliquant un expert. Notre objectif est la modélisation d'un ITS dont la simulation permettrait de vérifier les propriétés prouvées dans un scénario plus large et de générer sur les modèles des données susceptibles d'alimenter une boucle de preuve interactive. En guise de résultats préliminaires, nous présentons les modèles DEVS d'un réseaux ad hoc de véhicules, d'une méthode de clustering le structurant ainsi que la procédure de validation de ces modèles.