Abstract FR:

Dans cette these, nous proposons a la fois un modele et un langage, appeles ssl, pour la specification des systemes symetriques. Ssl est fortement inspiree d'estelle qui est une technique de description formelle normalisee par l'iso. A la difference d'estelle, ssl est fonde sur un concept de genericite complete, ce qui lui acquiert une aptitude a lui appliquer des methodes optimisees de verification. Notre demarche consiste a traduire automatiquement une specification ssl en un modele de reseaux de petri colores sur lequel sont basees nos methodes de verification. De la genericite du langage ssl decoule une propriete importante a savoir la symetrie de comportement des instances de processus. Cette propriete est exploitee pour appliquer des methodes optimisees de verification de protocoles. Ces dernieres consistent en la construction d'un graphe d'etat reduit appele graphe symbolique. La construction du graphe symbolique exploite les symetries de comportement des processus pour reduire la taille du graphe. Nous avons egalement defini un graphe symbolique etendu qui permet l'exploitation d'autres symetries de comportement qui ne sont pas exploitees par la premiere methode. Nous avons propose une modelisation du temps a l'aide du modele des reseaux colores. Cette modelisation consiste a representer une horloge globale d'un systeme par un sous-reseau de petri. Ainsi, la specification de contraintes temporelles dans ce systeme, decrit a l'aide de machines a etats finis communicantes, sont traduites pour donner un reseau colore uniforme. La semantique du temps adoptee est similaire a celle des reseaux de petri temporels; cette semantique a ete egalement utilisee dans la definition d'estelle. Un nouveau modele de reseaux interpretes a ete defini comme etant la base d'un outil, appele petristelle, de verification des specifications estelle. Petristelle prend en compte des fonctionnalites importantes d'estelle telles que le fonctionnement synchrone et la communication par files fifo. La generation d'un graphe synchrone est possible apres traduction en reseaux interpretes