Lors de la conférence brésilienne sur les méthodes formelles SBMF 2025 (2-5 décembre, Recife), l’Institut Metropole Digital – IMD/UFRN et CLEARSY présentent leurs travaux sur la vérification formelle du code C généré à partir d’un modèle formel en langage B.
Dans notre article intitulé « Bridging the B-Method and ACSL » (Concilier la méthode B et l’ACSL), nous montrons comment générer automatiquement des assertions ACSL à partir de modèles B afin de vérifier, avec Frama-C, que le code C conserve les propriétés formelles initialement définies.
Cette approche associe la modélisation formelle et l’analyse statique et garantit que le code embarqué critique répond à ses exigences de sécurité. Une étude de cas illustre son efficacité.
En combinant rigueur mathématique associée à des preuves et des outils modernes, CLEARSY poursuit son engagement en faveur de la sureté de fonctionnement et la sécurité basées sur l’innovation et les méthodes formelles.