Abstract FR:

Une technique de verification compare une entite operationnelle dont l'evolution est observable, avec une entite de reference qui sert d'oracle sur le comportement attendu. L'entite operationnelle est decrite par les reseaux de predicats et l'entite de reference par une logique temporelle arborescente