Valider la sûreté d’un système avant l’implémentation finale : c’est tout l’enjeu du Model Checking.
Cette méthode de vérification s’appuie sur un modèle formel pour analyser chaque évolution d’un système et s’assurer qu’il respecte bien un ensemble de propriétés critiques.
Dans notre dernier article, proposé par Nicolas Breton, nous abordons :
- Le modèle formel, comme spécification exempte d’ambiguïté.
- Le jumeau numérique pour la simulation fonctionnelle.
- La vérification de propriétés de sûreté.
- L’usage de Systerel Smart Solver (S3), notre outil basé sur le langage HLL.