Analyse et preuve d'intégrité d'exécution

Objectifs

• Preuve de l'absence d'erreur d'exécution
  • Débordement arithmétique
  • Division par zéro
  • Accès hors tableau
  • Autres RTE génériques
• Preuve de robustesse
  • Démonstration sur un modèle dont l'environnement n'est pas contraint (résistance à des entrées quelconques)
  • Preuve dans un environnement réaliste
  • Lorsque la démonstration de robustesse n'est pas possible, ajout de contraintes sur l'environnement pour prouver l'absence de RTE

Entrées

• Modèle (conception détaillée) de la fonction ou du système
  • E.g. modèle utilisé pour la génération de code

Résultats

• Preuve d'absence d'erreurs d'exécution
• Recommandations de corrections
• Scénarios de tests

Démarche

• Instrumentation du modèle avec des assertions de contrôle de RTE
• Co-simulation modèle et modèle instrumenté
• Détection de contre-exemple sur modèle instrumenté (recherche de RTE)
• Modélisation de l'environnement (ajout de contraintes en fonction des contre-exemples détectés)
• Preuve du modèle instrumenté dans l'environnement (ce dernier peut être vide en cas de robustesse)
• Génération de tests