Analyse et Preuve de propriétés globales sur un système

Objectifs

  • Formalisation des concepts système, des propriétés et de l'environnement
  • Démonstration des propriétés globales du système
    • Correction et conformité à des exigences de fonctionnement
      • Exemple : vivacité, disponibilité, respect de contraintes de séquencement ou de cohérence
    • Sécurité : respect d'exigences fonctionnelles de sécurité
      • Exemple : propriété d'anticollision (pour un système de pilotage automatique de trains CBTC)
    • Robustesse : maintien des états sûrs
      • Prise en compte des erreurs temporelles
      • Prise en compte des modes dégradés externes
      • Analyse des défaillances internes
      • Lien avec les AMDE fonctionnelles ou les Analyses fonctionnelles de sécurité
  • Détection d'erreurs de spécification
  • Vérification de cohérence entre le système et son environnement
  • Génération de tests

Entrées

  • Modèle (e.g. Simulink) du système, ou exigences fonctionnelles (spécification)
  • Hypothèses de comportement de l'environnement (ou modèle)
  • Propriétés cible
    • Propriétés issues du cahier des charges
      • Point de vue concepteur
    • Propriétés issues d'analyse de risque
      • Point de vue vérificateur

Résultats

  • Vérification de la tenue des propriétés
  • Identification des conditions (environnement) et des hypothèses sous lesquelles les propriétés tiennent
  • Scénarios de tests applicables au système
    • Couverture de l'environnement
    • Couverture des propriétés
    • Couverture du modèle
  • Mesures de couverture des tests en fonction de la stratégie de test
  • Rapport de preuve

Démarche

    La démarche est itérative, et basée sur les activités de modélisation, simulation, preuve, test, détection d'erreurs, ajout de contraintes:

  • Formalisation des propriétés dans le langage de modélisation, sous forme d'observateurs
  • Connexion des observateurs au modèle du système
  • Simulation modèle sous observateurs
  • Détection de contre-exemple sur modèle avec observateurs
  • Modélisation de l'environnement, en ajoutant si besoin les contraintes
  • Preuve de cohérence de l'environnement
  • Preuve des propriétés, sur le système dans son environnement
  • Génération de tests
  • Simulation des scénarios de tests et mesure effective du taux de couverture des tests, sur le système