Combinaison des avantages de la planification par Intelligence Artificielle pour assister l'analyse formelle préliminaire des vulnérabilités en cybersécurité des Systèmes de Contrôle Industriel

Cet article propose une approche novatrice et pratique pour vérifier la véracité et l'exhaustivité des spécifications fonctionnelles (l'exhaustivité signifie complète pour une fonction spécifiée), en particulier pour des systèmes critiques en matière de sécurité complexes. Cette approche combine la technique de planification en Intelligence Artificielle (IA) avec des spécifications fonctionnelles formelles, afin d'assister l'analyse des vulnérabilités en cybersécurité sur les Systèmes de Contrôle Industriel (SCI) critiques pour la sécurité. L'efficacité de cette combinaison est représentée par des exemples, basés sur une Machine de Rechargement (RM) critique pour la sécurité. Les RM sont largement utilisées dans les centrales nucléaires. Le résultat de cette idée est une spécification fonctionnelle correcte et complète de fonctions spécifiques, qui est la base clé pour notre analyse ultérieure des vulnérabilités en matière de sécurité et de sûreté, en particulier pour effectuer des analyses basées sur la vérification par modèle. Cette approche pratique de vérification est applicable à d'autres systèmes et plateformes d'Instrumentation & Contrôle (I&C).