RetourRetour

Méthodes de Validation


Cycle de développement d'un système

Validation dans le processus de développement d'un système


La modélisation formelle et les techniques de validation permettent la détection des erreurs de conception tôt dans le cycle de conception (gain de temps et d'argent).
De plus, la dimension formelle offre des possibilités supplémentaires en termes de représentation des systèmes et de fiabilité de leur analyse.

Méthodes de validation

  • Vérification de code : analyse minutieuse (souvent humaine) des lignes de code ou de l'implémentation.
  • Preuve : preuve de propriétés par l'utilisation de concepts purement mathématiques.

Méthodes de validation sur modèle formel du système :

  • Simulation : exécution du modèle, de façon aléatoire ou pas à pas (=> non exhaustif). La simulation est très pratique pour la détection des erreurs simples de modélisation. Mais l'inconvénient de cette technique est qu'elle ne fournie pas de preuve (une propriété observée sur un scénario n'est pas forcément toujours observable).
  • Model checking : analyse automatique exhaustive de tous les comportements possibles du système. Cette technique d'analyse est utilisable sur des formalismes "machines à états", comme les Réseaux de Petri ou les automates. Un graphe d'état ou de région peut être construit afin de représenter tous les états possibles du système modélisé. Puis le model checking consiste à parcourir exhaustivement ce graphe et de vérifier sur chacun des états s'il vérifie une propriété. Les propriétés du model checking sont en général exprimé en logique temporelle. Le principal inconvénient de cette méthode d'analyse est la difficulté d'application à des systèmes de taille et de compléxités réelles : le nombre d'états possibles devient rapidement exponentiel.
  • (Plus de détails sur le model checking et les méthodes d'analyse formelle dans ma thèse).
Méthodes de validation sur prototype du système :
  • Test : exécution du système sur un scénario de valeurs d'entrées spécifiques, et analyse des sorties observées.
  • Injection de fautes : le système est soumis à l'occurrence de nombreuses fautes ce qui permet de simuler un environnement réel perturbé.