À mesure que les systèmes embarqués et les composants logiciels critiques deviennent de plus en plus complexes et interconnectés, garantir leur exactitude et leur fiabilité est devenu un enjeu central, tant en matière de sûreté que de cybersécurité. Si les techniques de vérification classiques présentent souvent des limites en termes de garanties, les méthodes formelles offrent une approche fondée sur des bases mathématiques pour prouver des propriétés système ou détecter des violations de spécifications. Malgré leur puissance, ces méthodes sont parfois mal comprises ou perçues comme inaccessibles. Cet article propose une vue d’ensemble claire et structurée des méthodes formelles : leur fonctionnement, leurs apports et les raisons pour lesquelles leur adoption progresse dans le monde industriel.
Les méthodes formelles : de quoi s’agit-il ?
Les méthodes formelles sont un ensemble de techniques rigoureuses et automatisées, fondées sur l’abstraction mathématique, utilisées pour concevoir des systèmes logiciels ou matériels.
Elles remplacent ou complètent le raisonnement humain sur ces systèmes avec trois objectifs principaux:
synthétiser (générer) l’implémentation du système à partir d’une description formelle,
vérifier la conformité du système par rapport à sa description formelle,
prouver que l’implémentation du système respecte ses spécifications (ou propriétés).
Les méthodes formelles accélèrent le développement des systèmes tout en rendant leur implémentation plus fiable que les approches manuelles.
Ce document se concentre sur les méthodes formelles utilisées pour prouver l’absence ou détecter des violations de spécifications, qu’elles soient fonctionnelles, liées à la sûreté ou à la cybersécurité.
Les avantages des méthodes formelles par rapport aux preuves manuelles sont les suivants :
Sans erreur : les méthodes formelles ne sont pas sujettes aux erreurs de raisonnement comme peuvent l’être les êtres humains.
Reproductibles : elles donnent les mêmes résultats à chaque exécution de la preuve.
Accessibles : utiliser un outil de preuve demande moins d’expertise que de produire une preuve à la main.
L’avantage principal des méthodes formelles par rapport aux méthodes semi-formelles ou informelles est la garantie de détection de toutes les violations : toutes les propriétés cibles sont vérifiées sur tous les états du système, pour toutes les entrées possibles. La solidité et la complétude des résultats augmentent la fiabilité du système.
Les méthodes formelles se répartissent en trois grandes catégories :
La démonstration de théorèmes : consiste à produire des preuves formelles à partir d’une description du système, d’un ensemble d’axiomes et de règles d’inférence.
La vérification de modèles (model checking) : prouve que la description du système satisfait les propriétés (ou fournit un contre-exemple) pour tous les états possibles du système.
L’interprétation abstraite : vérifie des propriétés sur la description du système pour tous les chemins d’exécution et toutes les valeurs possibles des variables (lattices).
En mode preuve, les méthodes formelles concluent par :
« Vrai » : si la propriété est vérifiée pour tous les états du système,
« Faux » : s’il existe au moins un état qui viole la propriété.
En mode preuve, la vérification de modèles et l’interprétation abstraite peuvent également conclure par « Peut-être » si le raisonnement formel ne permet pas de conclure. Cette conclusion n’existe pas en démonstration de théorèmes.
En mode détection, les méthodes formelles identifient les états qui violent une propriété. Ce mode est uniquement disponible avec la vérification de modèles et l’interprétation abstraite. Il est utile pour le débogage : on peut détecter une première violation, la corriger, relancer l’analyse pour détecter la suivante, et ainsi de suite jusqu’à ce qu’aucune violation ne soit détectée, puis passer au mode preuve.
L’application à grande échelle des méthodes formelles sur des systèmes industriels complexes peut nécessiter une intervention humaine. Lorsque le raisonnement ne parvient pas à une conclusion « Vrai » ou « Faux », qu’il est trop long ou qu’il retourne « Peut-être », il est nécessaire d’enrichir la description initiale :
Pour la démonstration de théorèmes : ajouter des axiomes ou des règles d’inférence,
Pour la vérification de modèles : formuler des lemmes,
Pour l’interprétation abstraite : restreindre les domaines des variables d’entrée ou ajouter des assertions.
Pourquoi et comment utiliser les méthodes formelles ?
Les méthodes formelles contribuent grandement à la fiabilité et à la robustesse des systèmes logiciels ou matériels grâce à l’analyse mathématique sous-jacente.
Elles sont implémentées dans des outils de preuve qui masquent les fondements mathématiques.
Par exemple, les assistants de preuve sont basés sur la démonstration de théorèmes, les outils de modélisation (MBD) sur la vérification de modèles, et certains outils d’analyse statique sur l’interprétation abstraite.
Pour la vérification de modèles et l’interprétation abstraite, l’utilisateur final n’a pas besoin de connaître les théories sous-jacentes ; il est uniquement responsable de la description du système.
Pour la démonstration de théorèmes, la description initiale combine la description du système et la théorie de preuve. En conséquence, le niveau de connaissance mathématique requis de la part de l’utilisateur est plus élevé.
À noter : les trois catégories de méthodes peuvent être utilisées indépendamment ou de façon séquentielle dans une chaîne d’outils de preuve.
L’exécution de l’outil de preuve nécessite une configuration combinant la description du système et les paramètres de contrôle de la preuve.
Lors du premier lancement, l’outil peut ne pas conclure sur la validité d’une propriété système. Cela est généralement dû à une configuration incomplète.
L’utilisateur final doit alors compléter cette configuration pour définir la description du système et de son environnement (vérification de modèles ou interprétation abstraite), ou la théorie de preuve (démonstration de théorèmes), jusqu’à ce que l’outil puisse conclure.
Par conséquent, plusieurs lancements de l’outil peuvent être nécessaires avant de prouver si une propriété système est valide ou non.
Une fois cette configuration finalisée pour un système, elle pourra être réutilisée pour toutes les versions futures de ce système, ainsi que pour tous les systèmes « équivalents ».
Les outils de preuve basés sur les méthodes formelles produisent uniquement des conclusions telles que « Vrai » ou « Faux », sans démonstration associée.
Si la conclusion est « Faux », certains outils peuvent produire (sur demande) un ensemble de données représentatif déclenchant la violation de propriété.
En revanche, si la conclusion est « Vrai », aucun détail n’est automatiquement fourni, car la propriété est valide pour un ensemble trop vaste de données (chaque valeur d’entrée et tous les chemins d’exécution) pour être résumé simplement.
La vérification des résultats de preuve peut être réalisée par une « double chaîne de preuve », basée sur l’idée que si une propriété est prouvée sur un système par deux chaînes différentes, les conclusions peuvent être considérées comme fiables.
Cette méthode nécessite la preuve de l’équivalence des configurations et de l’indépendance des outils (issus de technologies différentes).
Une autre méthode consiste pour l’utilisateur final à choisir un outil de preuve certifié, disposant d’un kit de qualification, puis à démontrer que l’outil est utilisé conformément à son périmètre d’usage.
Les outils de preuve sont utilisés depuis longtemps pour vérifier des protocoles de communication ou des propriétés de sûreté sur les systèmes embarqués.
Leur usage est aujourd’hui recommandé voire exigé par un nombre croissant de normes, augmentant de facto le nombre d’industriels qui les utilisent, ainsi que les domaines d’application (cryptographie, aéronautique, automobile, énergie, défense, ferroviaire, etc.).
Lorsqu’une campagne de preuve a été lancée sur une révision d’un système, elle peut être facilement relancée sur les révisions suivantes.
Si la campagne initiale est généralement menée avec l’assistance d’un expert, les suivantes peuvent être effectuées sans aide, car les propriétés ont déjà été définies.
De plus, si la campagne couvre l’ensemble du système, toute différence comportementale entre révisions est capturée, automatiquement détectée, puis :
acceptée en modifiant la propriété,
ou rejetée en corrigeant le système.
Le choix de l’outil de preuve ou de sa configuration peut être confié à des experts pour qu’il soit en adéquation avec les objectifs de preuve et la description du système.
Conclusion
Les méthodes formelles ne sont plus confinées aux milieux académiques ou à des applications de niche. Avec l’essor des outils de vérification formelle et la pression réglementaire croissante dans des domaines comme l’avionique, l’automobile ou la cybersécurité, leur déploiement industriel est devenu à la fois viable et pertinent.
Au-delà de leur rigueur technique, leur véritable force réside dans la reproductibilité, la fiabilité et la profondeur d’analyse qu’elles offrent.
Lorsqu’elles sont correctement configurées et intégrées au cycle de développement, elles permettent aux organisations de détecter les défauts critiques en amont, de réduire les risques liés à la certification et d’améliorer la maintenabilité des systèmes sur le long terme.
Avec la montée en maturité des outils et l’émergence de bonnes pratiques, les méthodes formelles sont appelées à devenir un pilier de l’ingénierie logicielle de confiance.
