Développement d'une application pour le contrôle automatisé de l'appontage d'avions de chasse. Le projet utilise des méthodes formelles, notamment la méthode B, pour modéliser, valider et générer automatiquement du code source (Ada ou C++) garantissant la fiabilité des systèmes critiques. Il s'inscrit dans un cadre académique ou industriel exigeant une approche rigoureuse et sécurisée.