Abstract FR:

Dans cette these, nous allons presenter un nouvel environnement de validation de proprietes dynamiques de materiel appele chloe pour chronograms logic editor. Cet environnement est base sur la definition d'un nouveau langage graphique, inspire par un formalisme familier des concepteurs: les chronogrammes. Utilises depuis longtemps mais avec beaucoup de variantes, ils apparaissent comme un langage puissant et ergonomique dans la definition et l'edition d'un grand nombre de proprietes comportementales. Nous nous attacherons dans un premier temps a definir le langage chloe, de maniere formelle autant du point de vue de sa syntaxe que de sa semantique. Puis nous developperons les differentes utilisations possibles de ces proprietes dans une optique de specification, ou de verification de proprietes. Compose d'un editeur dirige par la syntaxe, et de deux decompilateurs dans les langages signal et vhdl, l'environnement chloe permet de generer facilement des analyseurs de traces qui permettent de verifier la validite des proprietes temporelles ainsi specifiees