Abstract FR:

Le langage de specification asn. 1 (abstract syntax notation one) est une norme conjointe de l'iso et de l'uit-t permettant une description des types des donnees susceptibles d'etre echangees au cours d'une transaction entre applications. La solution apportee a l'heterogeneite est donc symetrique : tous les participants partagent un ensemble de modules asn. 1 (constituant donc la partie donnee du protocole) independant de leur architecture locale, materielle ou logicielle. Ce partage s'etend par l'emploi commun d'un codage (encoding rules) des valeurs dont les types sont definis par la couche asn. 1. L'iso et l'uit-t publient plusieurs codages possibles pour les valeurs de type asn. 1. Ces codages sont eux aussi independants des architectures des entites communicantes, et sont des specifications de la serialisation des valeurs asn. 1, c'est-a-dire de la transformation des valeurs asn. 1 en flots de bits. Les compilateurs asn. 1 souffrent de non-conformite chronique par rapport a la norme (x. 680). Notre these est qu'une approche formelle, fondee sur des methodes en usage en theorie de la programmation, permet de clarifier totalement asn. 1 et de produire un analyseur de specifications conforme. D'une part, nous donnons une semantique operationnelle d'asn. 1 (x. 680), qui decrit aussi la phase d'analyse d'un compilateur asn. 1. Un outil d'analyse tres fine a ainsi ete realise en objective cam1 et utilise dans l'industrie. D'autre part nous formalisons les ber (basic encoding rules), ainsi qu'un decodage associe, puis nous prouvons que pour des valeurs bien typees, la composition du codage et du decodage est l'identite dans un noyau d'asn. 1 que nous precisons (ce noyau a la meme puissance d'expression que tout asn. 1). Ce theoreme est une garantie forte de la surete de la transmission. Ce travail de recherche montre aussi que formaliser permet de detecter des defauts de conception dans les langages, et de les corriger en participant aux comites de normalisation.