Validation et vérification du modèle
Commandes à réseaux de Petri - Modélisation

Un réseau de Petri représentant la commande du procédé a été obtenu par l’étape d’analyse et modélisation. Il a été construit par composition de fonctions ou de comportements qui caractérisent le fonctionnement de parties du système à commander.

Le modèle ainsi obtenu est réputé complet et censé répondre au fonctionnement attendu. Toutefois, est-ce que ce modèle fournit une description correcte de ce qui est souhaité ? Est-ce que la composition d’éléments de base n’a pas introduit de perturbation croisée de ces éléments ?

Pour cela, il faut valider ce résultat, pour tenter de mettre en évidence des erreurs éventuelles de modélisation, et confirmer la conformité du modèle aux spécifications du cahier des charges par la vérification de toutes les contraintes de départ.

Le modèle à réseau de Petri présente la particularité de pouvoir être analysé : à sa représentation graphique est associée une représentation numérique sur laquelle il est possible de mener des opérations analytiques formelles.

Comme il représente le comportement du système de commande, il peut aussi être simulé, c’est-à-dire être parcouru sans pour autant être relié au procédé, à la seule fin de vérifier que les cheminements qu’il est possible de parcourir restent cohérents au regard du fonctionnement attendu.

Il faut toutefois garder présent à l’esprit que la modélisation graphique manuscrite est nécessairement traduite par une méthode ou une autre de mise en œuvre, et il est alors très facile d’oublier de décrire (ou d’ajouter) un arc, de se tromper dans une pondération ou une expression logique. En cela, les méthodes de validation peuvent aussi être trompeuses dans la mesure où un réseau à analyser doit être traduit dans le langage de l’outil de vérification.

La plus grande attention doit donc être portée à la matérialisation du réseau de Petri, aussi bien dans sa description lors de la mise en œuvre que pour son analyse afin que, dans ce contexte, les méthodes de validation et vérification puissent apporter tout leur intérêt pour conclure sur la bonne description du modèle.