Analyse et Preuve de robustesse d'une fonction
Objectifs
- Démonstration de l'efficacité des protections niveau fonction
- 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 les pre/post
- Preuve de bon fonctionnement (pas de défaillance)
- Preuve en présence de défaillance d'une fonction quelconque
- Utilisation possible : preuve des ranges d'entrées / sorties
Entrées
- Modèle (spécification exécutable)
- Pour chaque fonction du modèle à étudier
- interfaces de la fonction
- Environnement
- Autres fonctions
- Hypothèses de comportement à étudier
- Assertions
- Propriétés locales
- Modes dégradés
Résultats
- Analyse de robustesse
- Recommandations de barrières de protection
- Scénarios de tests applicables à la fonction
Démarche
- Instrumentation du modèle avec des assertions de contrôle pre/post niveau fonction
- Co-simulation modèle et modèle instrumenté
- Détection de contre-exemple sur modèle instrumenté (recherche de violation d'assertion)
- 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)
- Preuves de bon fonctionnement locales
- preuves en présence de défaillance d'une fonction (analyse d'impact, vérification de confinement des défaillances locales d'une fonction)
- Génération de test
