Abstract FR:

La specification des services et protocoles de communication dans une architecture multi-couches, de type osi, est une problematique essentielle dans le contexte de la conception de reseaux d'ordinateurs. Il s'agit d'obtenir, a partir d'un ensemble de contraintes dites donnees initiales qui caracterisent le probleme pose, une specification operationnelle du couple service-protocole d'une couche donnee. Une methodologie de resolution de cette problematique a ete definie en termes d'etapes de synthese et de verification. La planification de ces etapes constitue une trajectoire de specification. Celle-ci se base sur l'integration progressive des contraintes donnees initiales et la verification de la specification issue de chaque etape de synthese par des contraintes de validite qui caracterisent une solution admissible. Deux types de trajectoires ont ete proposes, selon le style de la specification initiale du couple service-protocole: type operationnel et point de vue fournisseur du service; type oriente proprietes de connaissance et point de vue utilisateurs du service. Les activites de synthese et de verification ont ete elaborees pour ces deux trajectoires et formalisees en termes de systemes de transitions etiquettees, de logique temporelle et de logique epistemique. L'originalite de la deuxieme trajectoire de specification et l'utilisation de la logique epistemique ont ete mises en evidence. Une approche intelligence artificielle a permis de definir un modele conceptuel d'un systeme a base de connaissances pour la mise en uvre de la methodologie proposee. Il est structure selon trois niveaux de representation des connaissances relatifs au domaine, au raisonnement caracterisant les activites de synthese et de verification et a la planification des etapes d'une trajectoire de specification