Contribution à une démarche de vérification formelle d'architectures logicielles

Cette thèse propose une Démarche de Vérification Formelle d'Architectures Logicielles: DVFAL. La démarche DVFAL supporte divers formalismes de description d'architectures logicielles tels que: les ADL (langages de description d'architectures), UML2.0, Symphony et des profils UML2.0 dédiés au domaine des architectures logicielles. La démarche DVFAL préconise l'ADL Wright en tant que langage formel pivot permettant de représenter des architectures logicielles décrites dans les divers formalismes. En outre, elle propose des transformations de modèles sous forme des traducteurs (Wright vers CSP de Hoare et Wright vers Ada) pour bénéficier des outils de vérification des propriétés supportant CSP et Ada tels que FDR et FLAVERS. Enfin, la démarche DVFAL propose un profil UML2.0-Wright jouant le rôle d'un langage intermédiaire entre les formalismes à base d'UML et Wright.This thesis proposes a process for Formai Verification of Software Architectures: DVFAL. The DVFAL process supports various formalisms of description of software architectures as: the ADL (Architecture Description Language), UML2.0, Symphony and of the UML2.0 profiles dedicated ta the the software architectures domain. The DVFAL process recommends the Wright ADL as a pivot formai language permitting ta represent software architectures described in the various above stated formalisms. Besides, he proposes transformations of models into the translators (Wright toward CSP of Hoare and Wright toward Ada) to benefit from tools of verification of the properties supporting CSP and Ada as FDR and FLAVERS. Finally, the DVFAL process proposes a UML2.0-Wright profile playing the role of an intermediate language between the formalisms basis of UML and Wright.GRENOBLE1-BU Sciences (384212103) / SudocGRENOBLE-MI2S (384212302) / SudocSudocFranceF