Enhancing DO-178C Compliance in Safety-Critical Software: Integrating Formal Methods, Controlled Natural Language, and AI-Driven Automation

La dépendance croissante envers les Véhicules Aériens Sans Pilote (UAV) dans des secteurs tels que la défense, la logistique et la surveillance environnementale a intensifié la nécessité de normes strictes de certification logicielle pour garantir la sécurité et la fiabilité des opérations autonomes. La norme DO-178C, largement utilisée dans l’aviation, fournit un cadre rigoureux pour la certification des logiciels critiques, mettant l’accent sur la vérification, la validation et la traçabilité tout au long du cycle de vie logiciel. La conformité à la norme DO-178C est cruciale pour les UAV, qui fonctionnent souvent avec une supervision humaine limitée et nécessitent une prise de décision autonome fiable dans des conditions diversifiées et imprévisibles. Cependant, atteindre une conformité totale reste un défi en raison des ambiguïtés des spécifications en Langage Naturel (NL), de la nature fastidieuse des processus de vérification formelle, et de l’intégration limitée des outils automatisés, ce qui souligne la nécessité de méthodologies innovantes pour simplifier la vérification et améliorer la conformité. Cette recherche s’attaque à ces défis en proposant une avancée dans la conformité au DO- 178C pour les logiciels UAV grâce à des processus de vérification améliorés, une réduction des ambiguïtés du NL et une intégration accrue des outils automatisés. Un cadre méthodologique complet est proposé, combinant vérification formelle et automatisation pour rationaliser les flux de travail, améliorer la précision des exigences et renforcer la traçabilité pour un déploiement sûr des UAV dans des environnements complexes. Les contributions clés incluent un Langage Naturel Contrôlé (CNL) et un cadre de traduction basé sur l’intelligence artificielle pour convertir les exigences NL en logique temporelle, permettant une vérification robuste et évolutive. De plus, le jeu de données Natural2CTL est validé pour former des modèles d’apprentissage automatique, facilitant la traduction NL-CTL automatisée et réduisant les efforts de vérification manuels. Ces avancées représentent un progrès technologique et méthodologique dans la certification des UAV, avec des applications potentielles dans d’autres domaines logiciels critiques.