Contrôleur de feux de circulation d’un carrefour

Ce document traite de la spécification et de la vérification d’un contrôleur de feux de circulation pour un carrefour. Il s’adresse principalement aux étudiants et professionnels en informatique, en ingénierie des systèmes ou en automatisme, qui souhaitent comprendre comment modéliser et garantir le fonctionnement correct d’un système de feux tricolores.

La question

Le travail porte sur la définition précise du comportement d’un contrôleur de feux tricolores dans un carrefour. Le problème est de spécifier comment les feux doivent évoluer pour assurer la sécurité et la fluidité du trafic. Il s’agit d’éviter que des véhicules ne s’engagent simultanément sur des voies conflictuelles et de garantir que les véhicules ne restent pas bloqués indéfiniment. Ce problème est important car un mauvais contrôle des feux peut entraîner des accidents ou des embouteillages.

Concepts de base

Pour comprendre ce travail, il faut d’abord connaître quelques notions clés :

• Feux tricolores : chaque feu peut être dans l’un des trois états de couleur : rouge, jaune ou vert.
• État du contrôleur : le système peut être en service (es) ou hors service (hs). En hors service, tous les feux sont au jaune, signalant une panne ou une maintenance.
• Cycle des feux en service : les feux évoluent dans l’ordre rouge → vert → jaune → rouge.
• Conditions de sécurité (safety) : il ne doit jamais y avoir deux voies où les feux sont verts simultanément, empêchant ainsi les véhicules de s’engager en même temps sur des directions conflictuelles.
• Conditions de vivacité (liveness) : aucun feu ne doit rester rouge indéfiniment, ce qui garantirait que les véhicules ne soient pas bloqués sans fin.

Les variables principales sont feuA et feuB, représentant les feux de deux voies différentes, chacun prenant une valeur dans l’ensemble Couleur = {rouge, jaune, vert}. L’état global du contrôleur est une variable etat qui vaut soit es (en service), soit hs (hors service).

Approche

La méthode utilisée est une spécification formelle, décrivant précisément les états possibles et les transitions entre eux. Le système est modélisé comme une machine avec :

• Un ensemble de couleurs Couleur = {rouge, jaune, vert}.
• Une fonction Suiv qui définit la transition cyclique des couleurs :
  Suiv(rouge) = vert, Suiv(vert) = jaune, Suiv(jaune) = rouge.
• Des variables feuA et feuB représentant les couleurs actuelles des deux feux.
• Une définition claire des états hors service et en service :
• hs == feuA = jaune ∧ feuB = jaune
• es == service(feuA, feuB) ⇔ feuA = rouge ∧ feuB = rouge
• Des opérations permettant de changer l’état du contrôleur :
• Mise en service : transition de l’état hors service à l’état en service.
• Mise hors service : passage de l’état en service à l’état hors service.
• Changer feu : évolution des feux dans leur cycle, respectant la fonction Suiv et les conditions de sécurité.

Cette approche formelle permet de garantir que les propriétés de sécurité et de vivacité sont respectées, en imposant des invariants sur les variables et en contrôlant les transitions possibles.

Résultats

La spécification obtenue décrit un contrôleur de feux capable de :

• Maintenir les feux au jaune simultanément en hors service, assurant une signalisation claire en cas de panne.
• Faire évoluer les feux en service selon un cycle précis, garantissant que les deux feux ne soient jamais verts en même temps, ce qui assure la sécurité.
• Permettre la mise en service et la mise hors service de manière contrôlée.
• Respecter les conditions de vivacité, évitant que les véhicules restent bloqués indéfiniment.

Ces résultats sont formulés sous forme d’invariants et de préconditions dans la machine formelle, assurant que le système ne peut pas évoluer vers un état non sécurisé.

Limites et questions ouvertes

Le document ne détaille pas les aspects liés à la synchronisation avec d’autres carrefours ou à la gestion des flux de trafic en fonction de la densité. Il ne traite pas non plus des cas d’urgence ou d’intervention manuelle. Enfin, la spécification reste théorique et ne présente pas d’implémentation concrète ni de validation expérimentale.

Glossaire

• Couleur : ensemble des états possibles d’un feu (rouge, jaune, vert).
• FeuA, FeuB : variables représentant les couleurs des feux sur deux voies différentes.
• État (etat) : état global du contrôleur, soit en service (es), soit hors service (hs).
• Cycle des feux : ordre d’évolution des couleurs : rouge → vert → jaune → rouge.
• Condition de sécurité (safety) : propriété assurant qu’aucune voie ne soit verte simultanément avec une autre voie conflictuelle.
• Condition de vivacité (liveness) : propriété assurant que les véhicules ne restent pas bloqués indéfiniment.
• Fonction Suiv : fonction définissant la couleur suivante dans le cycle des feux.
• Machine formelle : modèle mathématique décrivant les états et transitions du système.