Transformation de modèles pour des applications aéronautiques et spatiales: vérification des propriétés

Le present article montre comment il est possible de s'appuyer sur la modelisation de la syntaxe et de la semantique les langages de programmation en UML et OCL pour verifier que les composants logiciels directement issus de la modelisation des exigences des applications aient bien toutes les qualites requises. Nous presentons ensuite sur deux applications en milieu industriel du domaine de l'aeronautique et du spatial comment les proprietes exigees de la part de ces composants peuvent etre exprimees et comment il est possible de verifier ces proprietes, avant la generation effective des codes de ces composants. Un exemple de prise en compte d'exigences metier concernant une application realisee dans le cadre du vehicule spatial de l'ATV est plus particulierement developpe.