Détection d'erreurs fonctionnelles C/C++

Objectifs

• Vérification de propriétés sur des fonctions critiques
  • Domaines de valeurs (E/S fonction)
  • Pré/Post-conditions
• Environnement fonctionnel
  • Contraintes nécessaires au respect des propriétés attendues

Bénéfices

• Détection d'erreurs de conception
• Vérification de propriétés fonctionnelles
• Calcul des domaines de valeurs sur les E/S des fonctions critiques
• Possibilité de mesurer la propagation d'un défaut vers d'autres fonctions
• Améliore la précision de l'analyse
• Conformité fonctionnelle des logiciels
• Optimisation de la validation & vérification
  • Tests et revue de pairs focalisés sur les aspects système & intégration
  • Intégration dans la démonstration de sécurité