Modélisation et Analyse de chroniques pour le diagnostic

Dans cet article nous proposons un modele de chronique qui peut etre vu comme une extension d'un Probleme Temporel Simple, permettant d'integrer dans les chroniques les contraintes d'interdiction representant l'absence d'un evenement dans l'ensemble du comportement modelise ou sur une partie predefinie. Sur la base de cette formalisation nous proposons des criteres permettant de caracteriser les chroniques et de les comparer afin d'evaluer la pertinence de la base de chroniques utilisee pour le diagnostic. En particulier nous proposons une methode d'analyse de diagnosticabilite reposant sur un test d'exclusivite des chroniques. Ce test permet de s'assurer que deux chroniques ne peuvent etre reconnues par un meme flux d'evenements genere par le systeme. Les chroniques sont modelisees par reseaux de Petri temporels et le test d'exclusivite est pose sous forme d'un probleme d'atteignabilite et resolu par une methode de verification automatique de modele.